1 /-
2 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Jens Wagemaker
5
6 Associated and irreducible elements.
7 -/
8 import algebra.group data.multiset
src └───────────┘ └───────────┘
9
10 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
11 open lattice
12
13 /-- is unit -/
14 def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
id └────┘ ┴ ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴
src └────┘ ┴ └───┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴
15
16 @[simp] lemma is_unit_unit [monoid α] (u : units α) : is_unit (u : α) := ⟨u, rfl⟩
id └────┘ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
src └────┘ └───┘ └─────┘ └─┘
typ └────┘ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
doc └──┘ └─────┘
17
18 theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
id └───────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ └───────┘ ┴ └┘
src └───────────┘ ┴ └─────┘ └──────────┘ └───────┘
typ └───────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ └───────┘ ┴ └┘
doc └─────┘ └───────┘
19
20 lemma is_unit.map [monoid α] [monoid β] (f : α →* β) {x : α} (h : is_unit x) : is_unit (f x) :=
id └────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴
src └────┘ └────┘ └┘ └─────┘ └─────┘
typ └────┘ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴
doc └┘ └─────┘ └─────┘
21 by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
id ┴ └──────────┘ └───────┘ ┴ ┴
src └─────┘ └────────────┘ └────┘└──────────┘┴ └───────┘┴ ┴ └─
typ └─────┘┴└────────────┘ └────┘└──────────┘┴ └───────┘┴┴┴┴└─
doc └─────┘ └────────────┘ └────┘ ┴ ┴ ┴ └─
txt └─────┘ └────────────┘ └────┘ ┴ ┴ ┴ └─
par └─────┘ └────────────┘ └────┘ ┴ ┴ ┴ └─
pid ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└
st └───────────────────────────────────────────────────────────
22
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
23 lemma is_unit.map' [monoid α] [monoid β] (f : α → β) {x : α} (h : is_unit x) [is_monoid_hom f] :
id └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────────┘ ┴
src └────┘ └────┘ └─────┘ └───────────┘
typ └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────────┘ ┴
doc └─────┘ └───────────┘
24 is_unit (f x) :=
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
doc └─────┘
25 h.map (monoid_hom.of f)
id ┴└──┘ └───────────┘ ┴
src └──┘ └───────────┘
typ ┴└──┘ └───────────┘ ┴
doc └───────────┘
26
27 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
id └──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └──────┘ └─────┘ ┴ ┴
typ └──────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └──┘ └─────┘
28 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
id ┴ ┴ ┴ └─┘ └──────┘
src ┴ ┴ └─┘ └──┘└──────┘└────┘
typ ┴ ┴ ┴ └─┘ └──┘└──────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴ └────┘
st └─────────────────┘
29 λ h, begin
id ┴
typ ┴
st └─────
30 haveI := subsingleton_of_zero_eq_one _ h,
id └─────────────────────────┘ ┴
src └───────┘└─────────────────────────┘└─┘
typ └───────┘└─────────────────────────┘└─┘┴
doc └───────┘└─────────────────────────┘└─┘
txt └───────┘ └─┘
par └───────┘ └─┘
pid ┴└─┘ └─┘
st ─────────────────────────────────────────┘└─
31 refine ⟨⟨0, 0, _, _⟩, rfl⟩; apply subsingleton.elim
id └─┘ └───────────────┘
src └─────┘ └───────────┘└─┘┴ └────┘└───────────────┘└
typ └─────┘ └───────────┘└─┘┴ └────┘└───────────────┘└
doc └─────┘ └───────────┘ ┴ └────┘ └
txt └─────┘ └───────────┘ ┴ └────┘ └
par └─────┘ └───────────┘ ┴ └────┘ └
pid ┴ └───────────┘ ┴ ┴ └
st ──────────────────────────────────────────────────────
32 end⟩
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘└─┘
33
34 @[simp] theorem not_is_unit_zero [nonzero_comm_ring α] : ¬ is_unit (0 : α) :=
id └───────────────┘ ┴ ┴ └─────┘ ┴
src └───────────────┘ ┴ └─────┘
typ └───────────────┘ ┴ ┴ └─────┘ ┴
doc └──┘ └───────────────┘ └─────┘
35 mt is_unit_zero_iff.1 zero_ne_one
id └┘ └──────────────┘┴ └─────────┘
src └┘ └──────────────┘┴ └─────────┘
typ └┘ └──────────────┘┴ └─────────┘
36
37 @[simp] theorem is_unit_one [monoid α] : is_unit (1:α) := ⟨1, rfl⟩
id └────┘ ┴ └─────┘ ┴ └─┘
src └────┘ └─────┘ └─┘
typ └────┘ ┴ └─────┘ ┴ └─┘
doc └──┘ └─────┘
38
39 theorem is_unit_of_mul_one [comm_monoid α] (a b : α) (h : a * b = 1) : is_unit a :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────────┘ ┴ ┴ └─────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
40 ⟨units.mk_of_mul_eq_one a b h, rfl⟩
id └────────────────────┘ ┴ ┴ ┴ └─┘
src └────────────────────┘ └─┘
typ └────────────────────┘ ┴ ┴ ┴ └─┘
41
42 theorem is_unit_iff_exists_inv [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, a * b = 1 :=
id └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └─────┘
43 ⟨by rintro ⟨⟨a, b, hab, _⟩, rfl⟩; exact ⟨b, hab⟩,
id ┴ └─┘
src └──────────────────────────┘ └────┘ └┘ ┴
typ └──────────────────────────┘ └────┘ ┴└┘└─┘┴
doc └──────────────────────────┘ └────┘ └┘ ┴
txt └──────────────────────────┘ └────┘ └┘ ┴
par └──────────────────────────┘ └────┘ └┘ ┴
pid └────────────────────┘ ┴ └┘ ┴
st └───────────────────────────────────────────┘
44 λ ⟨b, hab⟩, is_unit_of_mul_one _ b hab⟩
id ┴┴ └─┘ └────────────────┘
src └────────────────┘
typ ┴┴ └─┘ └────────────────┘
45
46 theorem is_unit_iff_exists_inv' [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, b * a = 1 :=
id └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └─────┘
47 by simp [is_unit_iff_exists_inv, mul_comm]
id └────────────────────┘ └──────┘
src └────┘└────────────────────┘└┘└──────┘└─
typ └────┘└────────────────────┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────────────
48
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
49 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
id └────┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └────┘ ┴ └─────┘ └─────┘ ┴
typ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘
50 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
id ┴┴ ┴ ┴
src ┴ └────┘
typ ┴┴ ┴ ┴ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴┴
st └─────┘
51
52 @[simp] theorem units.is_unit_mul_units [monoid α] (a : α) (u : units α) :
id └────┘ ┴ ┴ └───┘ ┴
src └────┘ └───┘
typ └────┘ ┴ ┴ └───┘ ┴
doc └──┘
53 is_unit (a * u) ↔ is_unit a :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
54 iff.intro
id └───────┘
src └───────┘
typ └───────┘
55 (assume ⟨v, hv⟩,
id ┴
typ ┴
56 have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [hv, units.coe_mul],
id └─────┘ ┴ ┴ ┴┴ ┴ ┴┴└┘ ┴ ┴ ┴└┘ └┘ └───────────┘
src └─────┘ ┴ ┴ ┴ ┴ └┘ └──────┘ ┴┴┴ └┘ └──┘ └┘└───────────┘┴
typ └─────┘ ┴ ┴ ┴┴ ┴ ┴┴└┘ └──────┘┴┴┴┴┴└┘ └──┘└┘└┘└───────────┘┴
doc └─────┘ └──────┘ ┴ ┴ └──┘ └┘ ┴
txt └──────┘ ┴ ┴ └──┘ └┘ ┴
par └──────┘ ┴ ┴ └──┘ └┘ ┴
pid ┴ ┴ ┴ └┘ └┘ ┴
st └────────────────────┘└┘└─────────────┘┴
57 by rwa [mul_assoc, units.mul_inv, mul_one] at this)
id └───────┘ └───────────┘ └─────┘
src └───┘└───────┘└┘└───────────┘└┘└─────┘└───────┘
typ └───┘└───────┘└┘└───────────┘└┘└─────┘└───────┘
doc └───┘ └┘ └┘ └───────┘
txt └───┘ └┘ └┘ └───────┘
par └───┘ └┘ └┘ └───────┘
pid └┘ └┘ └┘ ┴└──────┘
st └─────────────┘└─────────────┘└───────┘┴└──────┘
58 (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
id ┴┴ └┘ └───┘ ┴ ┴ ┴ └───────────┘ ┴ └──┘
src └───┘ ┴ ┴ └───────────┘ └──┘
typ ┴┴ └┘ └───┘ ┴ ┴ ┴ └───────────┘ ┴ └──┘
59
60 theorem is_unit_of_mul_is_unit_left {α} [comm_monoid α] {x y : α}
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
61 (hu : is_unit (x * y)) : is_unit x :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
62 let ⟨z, hz⟩ := is_unit_iff_exists_inv.1 hu in
id └─┘ ┴ └────────────────────┘┴ └┘
src └────────────────────┘┴
typ └─┘ ┴ └────────────────────┘┴ └┘
63 is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
id └────────────────────┘┴ ┴ ┴ └───────┘
src └────────────────────┘┴ ┴ └────┘└───────┘
typ └────────────────────┘┴ ┴ ┴ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid └─┘
st └──────────────┘
64
65 theorem is_unit_of_mul_is_unit_right {α} [comm_monoid α] {x y : α}
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
66 (hu : is_unit (x * y)) : is_unit y :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
67 @is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
id └─────────────────────────┘ ┴ ┴ └──────┘
src └─────────────────────────┘ └──┘└──────┘└
typ └─────────────────────────┘ ┴ ┴ └──┘└──────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └─────────────
68
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
69 theorem is_unit_iff_dvd_one [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └───────────┘ └─────┘ ┴ ┴
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
70 ⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
id └────────────┘
src └─────────────┘ └────┘ └─┘└────────────┘┴
typ └─────────────┘ └────┘ └─┘└────────────┘┴
doc └─────────────┘ └────┘ └─┘ ┴
txt └─────────────┘ └────┘ └─┘ ┴
par └─────────────┘ └────┘ └─┘ ┴
pid └───────┘ ┴ └─┘ ┴
st └─────────────────────────────────────────┘
71 λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
id ┴┴ ┴ ┴ └───┘ ┴ └──────┘ └─┘
src └───┘ └──┘ └┘└──────┘┴ └─┘
typ ┴┴ ┴ ┴ └───┘ └──┘┴└┘└──────┘┴ └─┘
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────┘└────────┘┴
72
73 theorem is_unit_iff_forall_dvd [comm_semiring α] {x : α} :
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
74 is_unit x ↔ ∀ y, x ∣ y :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
75 is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
id └─────────────────┘└────┘ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴
src └─────────────────┘└────┘ └───────┘ └─────┘
typ └─────────────────┘└────┘ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴
76
77 theorem mul_dvd_of_is_unit_left [comm_semiring α] {x y z : α} (h : is_unit x) : x * y ∣ z ↔ y ∣ z :=
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └─────┘ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
78 ⟨dvd_trans (dvd_mul_left _ _),
id └───────┘ └──────────┘
src └───────┘ └──────────┘
typ └───────┘ └──────────┘
79 dvd_trans $ by simpa using mul_dvd_mul_right (is_unit_iff_dvd_one.1 h) y⟩
id └───────┘ └───────────────┘ └─────────────────┘ ┴ ┴
src └───────┘ └──────────┘└───────────────┘┴ └─────────────────┘└─┘ └┘
typ └───────┘ └──────────┘└───────────────┘┴ └─────────────────┘└─┘┴└┘┴
doc └──────────┘ ┴ └─┘ └┘
txt └──────────┘ ┴ └─┘ └┘
par └──────────┘ ┴ └─┘ └┘
pid ┴└────┘ ┴ └─┘ └┘
st └────────────────────────────────────────────────────────┘
80
81 theorem mul_dvd_of_is_unit_right [comm_semiring α] {x y z : α} (h : is_unit y) : x * y ∣ z ↔ x ∣ z :=
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └─────┘ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
82 by rw [mul_comm, mul_dvd_of_is_unit_left h]
id └──────┘ └─────────────────────┘ ┴
src └──┘└──────┘└┘└─────────────────────┘┴ └─
typ └──┘└──────┘└┘└─────────────────────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────┘└─────────────────────────┘┴└
83
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
84 @[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───┘ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
85 mul_dvd_of_is_unit_left (is_unit_unit _)
id └─────────────────────┘ └──────────┘
src └─────────────────────┘ └──────────┘
typ └─────────────────────┘ └──────────┘
86
87 @[simp] lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───┘ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
88 mul_dvd_of_is_unit_right (is_unit_unit _)
id └──────────────────────┘ └──────────┘
src └──────────────────────┘ └──────────┘
typ └──────────────────────┘ └──────────┘
89
90 theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
91 (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
id ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴
src ┴ └─────┘ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
92 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
id └─────────────────┘┴ └───────┘ └┘ └─────────────────┘┴ └┘
src └─────────────────┘┴ └───────┘ └─────────────────┘┴
typ └─────────────────┘┴ └───────┘ └┘ └─────────────────┘┴ └┘
93
94 @[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
id ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └──┘ └─────┘
95 iff.intro
id └───────┘
src └───────┘
typ └───────┘
96 (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
id ┴┴ └┘ ┴ └──────────────┘ └─┘ └─┘
src └──────────────┘ └─┘ └─┘
typ ┴┴ └┘ ┴ └──────────────┘ └─┘ └─┘
97 (assume h, h.symm ▸ ⟨1, rfl⟩)
id ┴ ┴└───┘ ┴ └─┘
src └───┘ ┴ └─┘
typ ┴ ┴└───┘ ┴ └─┘
98
99 theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
id ┴ └─────┘ ┴ ┴ ┴└──────┘ ┴
src ┴ └─────┘ ┴ └──────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴└──────┘ ┴
doc └─────┘
100 ⟨λ ⟨u, hu⟩, (int.units_eq_one_or u).elim (by simp *) (by simp *),
id ┴┴ └─────────────────┘ └──┘
src └─────────────────┘ └──┘ └────┘ └────┘
typ ┴┴ └─────────────────┘ └──┘ └────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴┴ ┴┴
st └─────┘ └─────┘
101 λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
id ┴ └─────────────────┘┴ ┴ └──────────────────┘ ┴
src └─────────────────┘┴ └────┘└──────────────────┘└┘ ┴ └──┘
typ ┴ └─────────────────┘┴ ┴ └────┘└──────────────────┘└┘┴┴ └──┘
doc └────┘ └┘ ┴ └──┘
txt └────┘ └┘ ┴ └──┘
par └────┘ └┘ ┴ └──┘
pid └──┘ └┘ ┴
st └─────────────────────────┘└─┘┴└────┘
102
103 lemma is_unit_of_dvd_one [comm_semiring α] : ∀a ∣ 1, is_unit (a:α)
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴
src └───────────┘ ┴ └─────┘
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
104 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
id ┴ ┴ └┘ └────────────────────┘ └───┘ └─┘
src └┘ └────────────────────┘ └───┘ └─┘
typ ┴ ┴ └┘ └────────────────────┘ └───┘ └─┘
105
106 lemma dvd_and_not_dvd_iff [integral_domain α] {x y : α} :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
107 x ∣ y ∧ ¬y ∣ x ↔ x ≠ 0 ∧ ∃ d : α, ¬ is_unit d ∧ y = x * d :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
108 ⟨λ ⟨⟨d, hd⟩, hyx⟩, ⟨λ hx0, by simpa [hx0] using hyx, ⟨d,
id ┴ ┴ └┘ └─┘ └─┘ └─┘ └─┘
src └─────┘ └──────┘
typ ┴ ┴ └┘ └─┘ └─┘ └─────┘└─┘└──────┘└─┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └────────────────────┘
109 mt is_unit_iff_dvd_one.1 (λ ⟨e, he⟩, hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩), hd⟩⟩,
id └┘ └─────────────────┘┴ ┴┴ └┘ └───────┘ └┘ └─────┘
src └┘ └─────────────────┘┴ └──┘ └┘└───────┘└──┘ └┘└─────┘┴
typ └┘ └─────────────────┘┴ ┴┴ └──┘└┘└┘└───────┘└──┘└┘└┘└─────┘┴
doc └──┘ └┘ └──┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ ┴
st └─────┘└─────────┘└────┘└───────┘┴
110 λ ⟨hx0, d, hdu, hdx⟩, ⟨⟨d, hdx⟩, λ ⟨e, he⟩, hdu (is_unit_of_dvd_one _
id ┴└─┘ ┴ └─┘ └─┘ ┴┴ └────────────────┘
src └────────────────┘
typ ┴└─┘ ┴ └─┘ └─┘ ┴┴ └────────────────┘
111 ⟨e, (domain.mul_left_inj hx0).1 $ by conv {to_lhs, rw [he, hdx]};simp [mul_assoc]⟩)⟩⟩
id └─────────────────┘ ┴ └┘ └─┘ └───────┘
src └─────────────────┘ ┴ └────┘└────┘└┘└──┘ └┘ ┴┴ └────┘└───────┘┴
typ └─────────────────┘ ┴ └────┘└────┘└┘└──┘└┘└┘└─┘┴┴ └────┘└───────┘┴
doc └─────────────────┘ └────┘ ┴
txt └────┘└────┘└┘└──┘ └┘ ┴┴ └────┘ ┴
par └────┘└────┘└┘└──┘ └┘ ┴┴ └────┘ ┴
pid ┴└───────────┘ └┘ └┘ ┴┴ ┴
st └─────┘└────┘└──────┘└───┘ └┘└──────────────┘
112
113 lemma pow_dvd_pow_iff [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────────────┘ ┴ ┴ ┴ └─────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
114 x ^ n ∣ x ^ m ↔ n ≤ m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
115 begin
st └─────
116 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
117 { intro h, rw [← not_lt], intro hmn, apply h1,
id └────┘
src └─────┘ └────┘└────┘┴ └───────┘ └────┘
typ └─────┘ └────┘└────┘┴ └───────┘ └────┘
doc └─────┘ └────┘ ┴ └───────┘ └────┘
txt └─────┘ └────┘ ┴ └───────┘ └────┘
par └─────┘ └────┘ ┴ └───────┘ └────┘
pid └┘ └──┘ ┴ └──┘ ┴
st ───┘└─────┘└────────────┘└──────────┘└────────┘└─
118 have : x * x ^ m ∣ 1 * x ^ m,
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴┴┴ ┴┴┴ ┴┴└─┘ ┴ ┴ ┴
typ └─────┘ ┴┴┴ ┴┴┴ ┴┴└─┘ ┴┴┴ ┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ───────────────────────────────┘└─
119 { rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
id └──────┘ └─────┘ └───────┘ └─────────┘ └───────────────┘ └─┘ ┴
src └────┘└──────┘└┘└─────┘┴ └────┘└───────┘┴ └─────────┘└─┘ └───────────────┘┴ └─┘ ┴
typ └────┘└──────┘└┘└─────┘┴ └────┘└───────┘┴ └─────────┘└─┘ └───────────────┘┴└─┘└─┘┴┴
doc └────┘ └┘ ┴ └────┘ ┴ └─┘ ┴ └─┘ ┴
txt └────┘ └┘ ┴ └────┘ ┴ └─┘ ┴ └─┘ ┴
par └────┘ └┘ ┴ └────┘ ┴ └─┘ ┴ └─┘ ┴
pid └──┘ └┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
st ─────┘└────────────┘└───────┘└───────────────────────────────────────────────────────────┘└┘└
120 rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
id └───────────────────┘ └─────────────────┘ └─────────┘ ┴ └┘
src └───┘└───────────────────┘└──┘└─────────────────┘└───────┘ └────┘└─────────┘┴ ┴ ┴
typ └───┘└───────────────────┘└──┘└─────────────────┘└───────┘ └────┘└─────────┘┴┴┴└┘┴
doc └───┘└───────────────────┘└──┘ └───────┘ └────┘ ┴ ┴ ┴
txt └───┘ └──┘ └───────┘ └────┘ ┴ ┴ ┴
par └───┘ └──┘ └───────┘ └────┘ ┴ ┴ ┴
pid └┘ └──┘ ┴└──────┘ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─────────────────────┘┴└──────┘└───────────────────────┘└┘└
121 { apply pow_dvd_pow }
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────┘└─
122 end
st ──┘
123
124 /-- prime element of a semiring -/
125 def prime [comm_semiring α] (p : α) : Prop :=
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
126 p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
id ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
127
128 namespace prime
129
130 lemma ne_zero [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └───────────┘ └───┘ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc └───┘
131 hp.1
id └┘┴
src ┴
typ └┘┴
132
133 lemma not_unit [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴
src └───────────┘ └───┘ ┴ └─────┘
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴
doc └───┘ └─────┘
134 hp.2.1
id └┘┴ ┴
src ┴ ┴
typ └┘┴ ┴
135
136 lemma div_or_div [comm_semiring α] {p : α} (hp : prime p) {a b : α} (h : p ∣ a * b) :
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───┘ ┴ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
137 p ∣ a ∨ p ∣ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
138 hp.2.2 a b h
id └┘┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴
139
140 end prime
141
142 @[simp] lemma not_prime_zero [comm_semiring α] : ¬ prime (0 : α) :=
id └───────────┘ ┴ ┴ └───┘ ┴
src └───────────┘ ┴ └───┘
typ └───────────┘ ┴ ┴ └───┘ ┴
doc └──┘ └───┘
143 λ h, h.ne_zero rfl
id ┴ ┴└──────┘ └─┘
src └──────┘ └─┘
typ ┴ ┴└──────┘ └─┘
144
145 @[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
id └───────────┘ ┴ ┴ └───┘ ┴
src └───────────┘ ┴ └───┘
typ └───────────┘ ┴ ┴ └───┘ ┴
doc └──┘ └───┘
146 λ h, h.not_unit is_unit_one
id ┴ ┴└───────┘ └─────────┘
src └───────┘ └─────────┘
typ ┴ ┴└───────┘ └─────────┘
147
148 lemma exists_mem_multiset_dvd_of_prime [comm_semiring α] {s : multiset α} {p : α} (hp : prime p) :
id └───────────┘ ┴ └──────┘ ┴ ┴ └───┘ ┴
src └───────────┘ └──────┘ └───┘
typ └───────────┘ ┴ └──────┘ ┴ ┴ └───┘ ┴
doc └──────┘ └───┘
149 p ∣ s.prod → ∃a∈s, p ∣ a :=
id ┴ ┴ ┴└───┘ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴└───┘ ┴┴ ┴┴ ┴ ┴ ┴
doc └───┘
150 multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
id └───────────────────┘ ┴ ┴ └┘└───────┘ └────────────────┘ ┴ └──┘
src └───────────────────┘ └───────┘ └────────────────┘ └──┘
typ └───────────────────┘ ┴ ┴ └┘└───────┘ └────────────────┘ ┴ └──┘
151 assume a s ih h,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
152 have p ∣ a * s.prod, by simpa using h,
id ┴ ┴ ┴ ┴ ┴└───┘ ┴
src ┴ ┴ └───┘ └──────────┘
typ ┴ ┴ ┴ ┴ ┴└───┘ └──────────┘┴
doc └───┘ └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────┘
153 match hp.div_or_div this with
id └┘└─────────┘ └──┘
src └─────────┘
typ └┘└─────────┘ └──┘
154 | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
id └────┘ ┴ ┴ └────────────────────┘ ┴ ┴
src └────┘ └────────────────────┘
typ └────┘ ┴ ┴ └────────────────────┘ ┴ ┴
155 | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
id └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘ └──────────────────────┘
src └────┘ └──────────────────────┘
typ └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘ └──────────────────────┘
156 end
157
158 /-- `irreducible p` states that `p` is non-unit and only factors into units.
159
160 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
161 monoid allows us to reuse irreducible for associated elements.
162 -/
163 @[class] def irreducible [monoid α] (p : α) : Prop :=
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
164 ¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
165
166 namespace irreducible
167
168 lemma not_unit [monoid α] {p : α} (hp : irreducible p) : ¬ is_unit p :=
id └────┘ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴
src └────┘ └─────────┘ ┴ └─────┘
typ └────┘ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
169 hp.1
id └┘┴
src ┴
typ └┘┴
170
171 lemma is_unit_or_is_unit [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
id └────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └─────────┘ ┴ ┴
typ └────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘
172 is_unit a ∨ is_unit b :=
id └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
173 hp.2 a b h
id └┘┴ ┴ ┴ ┴
src ┴
typ └┘┴ ┴ ┴ ┴
174
175 end irreducible
176
177 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
id └────┘ ┴ ┴ └─────────┘ ┴
src └────┘ ┴ └─────────┘
typ └────┘ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
178 by simp [irreducible]
id └─────────┘
src └────┘└─────────┘└─
typ └────┘└─────────┘└─
doc └────┘└─────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────
179
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
180 @[simp] theorem not_irreducible_zero [semiring α] : ¬ irreducible (0 : α)
id └──────┘ ┴ ┴ └─────────┘ ┴
src └──────┘ ┴ └─────────┘
typ └──────┘ ┴ ┴ └─────────┘ ┴
doc └──┘ └─────────┘
181 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
id └─┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ └──────┘ └──┘
src └─────┘ ┴ └─────┘ └──────┘ └──┘
typ └─┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ └──────┘ └──┘
doc └─────┘ └─────┘
182 this.elim hn0 hn0
id └──┘└───┘
src └───┘
typ └──┘└───┘
183
184 theorem irreducible.ne_zero [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
id └──────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └──────┘ └─────────┘ ┴
typ └──────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
doc └─────────┘
185 | _ hp rfl := not_irreducible_zero hp
id └┘ └─┘ └──────────────────┘
src └─┘ └──────────────────┘
typ └┘ └─┘ └──────────────────┘
186
187 theorem of_irreducible_mul {α} [monoid α] {x y : α} :
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
188 irreducible (x * y) → is_unit x ∨ is_unit y
id └─────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─────────┘ ┴ └─────┘ ┴ └─────┘
typ └─────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────────┘ └─────┘ └─────┘
189 | ⟨_, h⟩ := h _ _ rfl
id ┴ └─┘
src └─┘
typ ┴ └─┘
190
191 theorem irreducible_or_factor {α} [monoid α] (x : α) (h : ¬ is_unit x) :
id └────┘ ┴ ┴ ┴ └─────┘ ┴
src └────┘ ┴ └─────┘
typ └────┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
192 irreducible x ∨ ∃ a b, ¬ is_unit a ∧ ¬ is_unit b ∧ a * b = x :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └─────┘ └─────┘
193 begin
st └─────
194 haveI := classical.dec,
id └───────────┘
src └───────┘└───────────┘
typ └───────┘└───────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ───────────────────────┘└─
195 refine or_iff_not_imp_right.2 (λ H, _),
id └──────────────────┘
src └─────┘└──────────────────┘└─┘ └────┘
typ └─────┘└──────────────────┘└─┘ └────┘
doc └─────┘ └─┘ └────┘
txt └─────┘ └─┘ └────┘
par └─────┘ └─┘ └────┘
pid ┴ └─┘ └────┘
st ───────────────────────────────────────┘└─
196 simp [h, irreducible] at H ⊢,
id ┴ └─────────┘
src └────┘ └┘└─────────┘└──────┘
typ └────┘┴└┘└─────────┘└──────┘
doc └────┘ └┘└─────────┘└──────┘
txt └────┘ └┘ └──────┘
par └────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st ─────────────────────────────┘└─
197 refine λ a b h, classical.by_contradiction $ λ o, _,
id └────────────────────────┘
src └─────┘ └──────┘└────────────────────────┘┴ ┴ └───┘
typ └─────┘ └──────┘└────────────────────────┘┴ ┴ └───┘
doc └─────┘ └──────┘ ┴ ┴ └───┘
txt └─────┘ └──────┘ ┴ ┴ └───┘
par └─────┘ └──────┘ ┴ ┴ └───┘
pid ┴ └──────┘ ┴ ┴ └───┘
st ────────────────────────────────────────────────────┘└─
198 simp [not_or_distrib] at o,
id └────────────┘
src └────┘└────────────┘└────┘
typ └────┘└────────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴┴ ┴┴└──┘
st ───────────────────────────┘└─
199 exact H _ o.1 _ o.2 h.symm
id ┴ ┴ └────┘
src └────┘ └─┘ └───┘ └─┘└────┘┴
typ └────┘┴└─┘ └───┘┴└─┘└────┘┴
doc └────┘ └─┘ └───┘ └─┘ ┴
txt └────┘ └─┘ └───┘ └─┘ ┴
par └────┘ └─┘ └───┘ └─┘ ┴
pid ┴ └─┘ └───┘ └─┘ ┴
st ────────────────────────────┘
200 end
st └─┘
201
202 lemma irreducible_of_prime [integral_domain α] {p : α} (hp : prime p) : irreducible p :=
id └─────────────┘ ┴ ┴ └───┘ ┴ └─────────┘ ┴
src └─────────────┘ └───┘ └─────────┘
typ └─────────────┘ ┴ ┴ └───┘ ┴ └─────────┘ ┴
doc └───┘ └─────────┘
203 ⟨hp.not_unit, λ a b hab,
id └┘└───────┘ ┴ ┴ └─┘
src └───────┘
typ └┘└───────┘ ┴ ┴ └─┘
204 (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.div_or_div (hab ▸ (dvd_refl _))).elim
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘└─────────┘ └─┘ ┴ └──────┘ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └──────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘└─────────┘ └─┘ ┴ └──────┘ └──┘
205 (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2
id ┴┴ └────┘ └─────────────────┘┴
src └────┘ └─────────────────┘┴
typ ┴┴ └────┘ └─────────────────┘┴
206 ⟨x, (domain.mul_left_inj (show a ≠ 0, from λ h, by simp [*, prime] at *)).1
id └─────────────────┘ ┴ ┴ ┴ └───┘ ┴
src └─────────────────┘ ┴ └───────┘└───┘└────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴ └───────┘└───┘└────┘ ┴
doc └─────────────────┘ └───────┘└───┘└────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└──┘ ┴┴└──┘
st └───────────────────┘
207 $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))
id └┘ └──────┘ └───────┘ └───────────┘
src └────┘└────┘└┘└─┘ ┴ └────┘└──────┘└┘└───────┘└┘└───────────┘┴
typ └────┘└────┘└┘└─┘└┘┴ └────┘└──────┘└┘└───────┘└┘└───────────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘└────┘└┘└─┘ ┴ └────┘ └┘ └┘ ┴
par └────┘└────┘└┘└─┘ ┴ └────┘ └┘ └┘ ┴
pid ┴└──────────┘ ┴ ┴┴ └┘ └┘ ┴
st └─────┘└────┘└─────┘└┘└────────────────────────────────────────┘
208 (λ ⟨x, hx⟩, or.inl (is_unit_iff_dvd_one.2
id ┴┴ └────┘ └─────────────────┘┴
src └────┘ └─────────────────┘┴
typ ┴┴ └────┘ └─────────────────┘┴
209 ⟨x, (domain.mul_left_inj (show b ≠ 0, from λ h, by simp [*, prime] at *)).1
id └─────────────────┘ ┴ ┴ ┴ └───┘ ┴
src └─────────────────┘ ┴ └───────┘└───┘└────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴ └───────┘└───┘└────┘ ┴
doc └─────────────────┘ └───────┘└───┘└────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└──┘ ┴┴└──┘
st └───────────────────┘
210 $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))⟩
id └┘ └──────┘ └───────┘ └───────────┘
src └────┘└────┘└┘└─┘ ┴ └────┘└──────┘└┘└───────┘└┘└───────────┘┴
typ └────┘└────┘└┘└─┘└┘┴ └────┘└──────┘└┘└───────┘└┘└───────────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘└────┘└┘└─┘ ┴ └────┘ └┘ └┘ ┴
par └────┘└────┘└┘└─┘ ┴ └────┘ └┘ └┘ ┴
pid ┴└──────────┘ ┴ ┴┴ └┘ └┘ ┴
st └─────┘└────┘└─────┘└┘└────────────────────────────────────────┘
211
212 lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [integral_domain α] {p : α} (hp : prime p) {a b : α}
id └─────────────┘ ┴ ┴ └───┘ ┴ ┴
src └─────────────┘ └───┘
typ └─────────────┘ ┴ ┴ └───┘ ┴ ┴
doc └───┘
213 {k l : ℕ} : p ^ k ∣ a → p ^ l ∣ b → p ^ ((k + l) + 1) ∣ a * b →
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
214 p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
215 λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩,
id ┴┴ ┴┴ ┴┴
typ ┴┴ ┴┴ ┴┴
216 have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
217 by simpa [mul_comm, _root_.pow_add, hx, hy, mul_assoc, mul_left_comm] using hz,
id └──────┘ └────────────┘ └┘ └┘ └───────┘ └───────────┘ └┘
src └─────┘└──────┘└┘└────────────┘└┘ └┘ └┘└───────┘└┘└───────────┘└──────┘
typ └─────┘└──────┘└┘└────────────┘└┘└┘└┘└┘└┘└───────┘└┘└───────────┘└──────┘└┘
doc └─────┘ └┘ └┘ └┘ └┘ └┘ └──────┘
txt └─────┘ └┘ └┘ └┘ └┘ └┘ └──────┘
par └─────┘ └┘ └┘ └┘ └┘ └┘ └──────┘
pid ┴┴ └┘ └┘ └┘ └┘ └┘ ┴┴└────┘
st └──────────────────────────────────────────────────────────────────────────┘
218 have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.ne_zero,
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └┘└──────┘
src ┴ ┴ ┴ └─────────┘ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └┘└──────┘
219 have hpd : p ∣ x * y, from ⟨z, by rwa [domain.mul_left_inj hp0] at h⟩,
id ┴ ┴ ┴ └─────────────────┘ └─┘
src ┴ ┴ └───┘└─────────────────┘┴ └────┘
typ ┴ ┴ ┴ └───┘└─────────────────┘┴└─┘└────┘
doc └───┘└─────────────────┘┴ └────┘
txt └───┘ ┴ └────┘
par └───┘ ┴ └────┘
pid └┘ ┴ ┴└───┘
st └───────────────────────────┘┴└───┘
220 (hp.div_or_div hpd).elim
id └┘└─────────┘ └─┘ └──┘
src └─────────┘ └──┘
typ └┘└─────────┘ └─┘ └──┘
221 (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
id ┴┴ └────┘ └─────────────┘ └──────┘ └───────────┘ └───────┘
src └────┘ └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘┴
typ ┴┴ └────┘ └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘┴
doc └───────┘ └┘ └┘ └┘ ┴
txt └───────┘ └┘ └┘ └┘ ┴
par └───────┘ └┘ └┘ └┘ ┴
pid ┴└──┘ └┘ └┘ └┘ ┴
st └────────────────────────────────────────────────────────────┘
222 (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
id ┴┴ └────┘ └─────────────┘ └──────┘ └───────────┘ └───────┘
src └────┘ └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘┴
typ ┴┴ └────┘ └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘┴
doc └───────┘ └┘ └┘ └┘ ┴
txt └───────┘ └┘ └┘ └┘ ┴
par └───────┘ └┘ └┘ └┘ ┴
pid ┴└──┘ └┘ └┘ └┘ ┴
st └────────────────────────────────────────────────────────────┘
223
224 def associated [monoid α] (x y : α) : Prop := ∃u:units α, x * u = y
id └────┘ ┴ ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └───┘ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ └───┘ ┴┴ ┴ ┴ ┴ ┴ ┴
225
226 local infix ` ~ᵤ ` : 50 := associated
id └────────┘
src └────────┘
typ └────────┘
227
228 namespace associated
229
230 @[refl] protected theorem refl [monoid α] (x : α) : x ~ᵤ x := ⟨1, by simp⟩
id └────┘ ┴ ┴ ┴ └┘ ┴
src └──┘ └────┘ └┘ └──┘
typ └────┘ ┴ ┴ ┴ └┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
231
232 @[symm] protected theorem symm [monoid α] : ∀{x y : α}, x ~ᵤ y → y ~ᵤ x
id └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └──┘ └────┘ ┴ └┘ └┘
typ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘
233 | x _ ⟨u, rfl⟩ := ⟨u⁻¹, by rw [mul_assoc, units.mul_inv, mul_one]⟩
id ┴ └─┘ └┘ └───────┘ └───────────┘ └─────┘
src └─┘ └┘ └──┘└───────┘└┘└───────────┘└┘└─────┘┴
typ ┴ └─┘ └┘ └──┘└───────┘└┘└───────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └────────────┘└─────────────┘└───────┘┴
234
235 @[trans] protected theorem trans [monoid α] : ∀{x y z : α}, x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
id └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └───┘ └────┘ ┴ └┘ └┘ └┘
typ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └───┘
236 | x _ _ ⟨u, rfl⟩ ⟨v, rfl⟩ := ⟨u * v, by rw [units.coe_mul, mul_assoc]⟩
id ┴ ┴ └─┘ ┴ └───────────┘ └───────┘
src └─┘ ┴ └──┘└───────────┘└┘└───────┘┴
typ ┴ ┴ └─┘ ┴ └──┘└───────────┘└┘└───────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────────┘└─────────┘┴
237
238 protected def setoid (α : Type*) [monoid α] : setoid α :=
id └────┘ ┴ └────┘ ┴
src └────┘ └────┘
typ └────┘ ┴ └────┘ ┴
239 { r := associated, iseqv := ⟨associated.refl, λa b, associated.symm, λa b c, associated.trans⟩ }
id └────────┘ └─────────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └──────────────┘
src └────────┘ └─────────────┘ └─────────────┘ └──────────────┘
typ └────────┘ └─────────────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └──────────────┘
240
241 end associated
242
243 local attribute [instance] associated.setoid
id └───────────────┘
src └───────────────┘
typ └───────────────┘
244
245 theorem unit_associated_one [monoid α] {u : units α} : (u : α) ~ᵤ 1 := ⟨u⁻¹, units.mul_inv u⟩
id └────┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴└┘ └───────────┘ ┴
src └────┘ └───┘ └┘ └┘ └───────────┘
typ └────┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴└┘ └───────────┘ ┴
246
247 theorem associated_one_iff_is_unit [monoid α] {a : α} : (a : α) ~ᵤ 1 ↔ is_unit a :=
id └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴
src └────┘ └┘ ┴ └─────┘
typ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴
doc └─────┘
248 iff.intro
id └───────┘
src └───────┘
typ └───────┘
249 (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, one_mul _⟩)
id ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─────┘
src └───┘ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─────┘
250 (assume ⟨c, h⟩, associated.symm ⟨c, by simp [h]⟩)
id ┴┴ └─────────────┘ ┴
src └─────────────┘ └────┘ ┴
typ ┴┴ └─────────────┘ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
251
252 theorem associated_zero_iff_eq_zero [comm_semiring α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └───────────┘ └┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
253 iff.intro
id └───────┘
src └───────┘
typ └───────┘
254 (assume h, let ⟨u, h⟩ := h.symm in by simpa using h.symm)
id ┴ └─┘ ┴└───┘ └────┘
src └───┘ └──────────┘└────┘
typ ┴ └─┘ ┴└───┘ └──────────┘└────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └─────────────────┘
255 (assume h, h ▸ associated.refl a)
id ┴ ┴ ┴ └─────────────┘ ┴
src ┴ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴
256
257 theorem associated_one_of_mul_eq_one [comm_monoid α] {a : α} (b : α) (hab : a * b = 1) : a ~ᵤ 1 :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └─────────┘ ┴ ┴ └┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
258 show (units.mk_of_mul_eq_one a b hab : α) ~ᵤ 1, from unit_associated_one
id └────────────────────┘ ┴ ┴ └─┘ ┴ └┘ └─────────────────┘
src └────────────────────┘ └┘ └─────────────────┘
typ └────────────────────┘ ┴ ┴ └─┘ ┴ └┘ └─────────────────┘
259
260 theorem associated_one_of_associated_mul_one [comm_monoid α] {a b : α} :
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
261 a * b ~ᵤ 1 → a ~ᵤ 1
id ┴ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ └┘ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘
262 | ⟨u, h⟩ := associated_one_of_mul_eq_one (b * u) $ by simpa [mul_assoc] using h
id ┴ └──────────────────────────┘ ┴ ┴ └───────┘ ┴
src └──────────────────────────┘ ┴ └─────┘└───────┘└──────┘ └
typ ┴ └──────────────────────────┘ ┴ ┴ └─────┘└───────┘└──────┘┴└
doc └─────┘ └──────┘ └
txt └─────┘ └──────┘ └
par └─────┘ └──────┘ └
pid ┴┴ ┴┴└────┘ └
st └──────────────────────────
263
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
264 lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
265 a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └┘
src └┘ └┘ ┴ └┘ ┴
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └┘
266 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
id └┘ └┘ ┴ └───────┘ └──────┘ └───────────┘
src ┴ └────┘ └┘ └┘└───────┘└┘└──────┘└┘└───────────┘┴
typ └┘ └┘ ┴ └────┘└─────┘└┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────┘
267
268 theorem associated_of_dvd_dvd [integral_domain α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─────────────┘ ┴ ┴ └┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
269 begin
st └─────
270 haveI := classical.dec_eq α,
id └──────────────┘ ┴
src └───────┘└──────────────┘┴
typ └───────┘└──────────────┘┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st ────────────────────────────┘└─
271 rcases hab with ⟨c, rfl⟩,
id └─┘
src └─────┘ └────────────┘
typ └─────┘└─┘└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ─────────────────────────┘└─
272 rcases hba with ⟨d, a_eq⟩,
id └─┘
src └─────┘ └─────────────┘
typ └─────┘└─┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ──────────────────────────┘└─
273 by_cases ha0 : a = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────┘└─
274 { simp [*] at * },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴└─┘┴└──┘┴
st ───┘└────────────┘└┘└
275 have : a * 1 = a * (c * d),
id ┴ ┴ ┴ ┴
src └─────┘ ┴┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴┴└─┘ ┴┴┴ ┴ ┴┴ ┴┴┴
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────┘└─
276 { simpa [mul_assoc] using a_eq },
id └───────┘ └──┘
src └─────┘└───────┘└──────┘ ┴
typ └─────┘└───────┘└──────┘└──┘┴
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st ───┘└───────────────────────────┘└┘└
277 have : 1 = (c * d), from eq_of_mul_eq_mul_left ha0 this,
id ┴ ┴ └───────────────────┘ └─┘ └──┘
src └───────┘ ┴ ┴ ┴ ┴ └───┘└───────────────────┘┴ ┴
typ └───────┘ ┴ ┴┴ ┴┴┴ └───┘└───────────────────┘┴└─┘┴└──┘
doc └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
pid └───┘└──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
st ───────────────────┘└───────────────────────────────────┘└─
278 exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
id └────────────────────┘ ┴ ┴ └───────┘ └────────────────────┘ └───────────┘
src └────┘ └────────────────────┘┴ ┴ ┴ └───────┘└─┘ ┴└──┘└────────────────────┘└┘└───────────┘┴└┘
typ └────┘ └────────────────────┘┴┴┴┴┴ └───────┘└─┘ ┴└──┘└────────────────────┘└┘└───────────┘┴└┘
doc └────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└┘
txt └────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└┘
par └────┘ ┴ ┴ ┴ └─┘ ┴└──┘ └┘ ┴└┘
pid ┴ ┴ ┴ ┴ └─┘ └───┘ └┘ └┘┴
st ──────────────────────────────────────────────────┘└─────────────────────────┘└─────────────┘┴└┘
279 end
st └─┘
280
281 lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
282 (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
id └───┘ ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴┴ ┴ └┘ ┴
src └───┘ └──────┘ ┴ └───┘ ┴ └───┘ ┴ ┴ └┘
typ └───┘ ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴┴ ┴ └┘ ┴
doc └───┘ └──────┘ └───┘ └───┘
283 multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
id └───────────────────┘ ┴ └┘ └─────────────────┘ └─────────┘
src └───────────────────┘ └────┘└┘┴└─────────────────┘└─┘└─────────┘┴
typ └───────────────────┘ ┴ └────┘└┘┴└─────────────────┘└─┘└─────────┘┴
doc └────┘ ┴ └─┘ ┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴┴ ┴ └─┘ ┴
st └──────────────────────────────────────────┘
284 (λ a s ih hs hps, begin
id ┴ ┴ └┘ └┘ └─┘
typ ┴ ┴ └┘ └┘ └─┘
st └─────
285 rw [multiset.prod_cons] at hps,
id └────────────────┘
src └──┘└────────────────┘└──────┘
typ └──┘└────────────────┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid └┘ ┴└─────┘
st ─────────────────────────┘┴└─────┘└─
286 cases hp.div_or_div hps with h h,
id └───────────┘ └─┘
src └────┘└───────────┘┴ └───────┘
typ └────┘└───────────┘┴└─┘└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ───────────────────────────────────┘└─
287 { use [a, by simp],
id ┴
src └───┘ └┘ ┴└──┘┴
typ └───┘┴└┘ ┴└──┘┴
doc └───┘ └┘ ┴└──┘┴
txt └───┘ └┘ ┴└──┘┴
par └───┘ └┘ ┴└──┘┴
pid └┘ └┘ └────┘
st ─────┘└────────┘└───┘┴└─
288 cases h with u hu,
id ┴
src └────┘ └────────┘
typ └────┘┴└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ──────────────────────┘└─
289 cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
id └──────────────────┘ └┘ ┴ └───────────────┘
src └────┘ └──────────────────┘┴ ┴ ┴ └───────────────┘└──
typ └────┘ └──────────────────┘┴ └┘┴┴┴ └───────────────┘└──
doc └────┘ ┴ ┴ ┴ └──
txt └────┘ ┴ ┴ ┴ └──
par └────┘ ┴ ┴ ┴ └──
pid ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────
290 (or.inl rfl)))).2 p u hu).resolve_left hp.not_unit with v hv,
id └────┘ └─┘ ┴ ┴ └┘ └─────────┘
src ───────┘ └────┘┴└─┘└─────┘ ┴ ┴ └─────────────┘└─────────┘└────────┘
typ ───────┘ └────┘┴└─┘└─────┘┴┴┴┴└┘└─────────────┘└─────────┘└────────┘
doc ───────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ └────────┘
txt ───────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ └────────┘
par ───────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ └────────┘
pid ───────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ └────────┘
st ───────────────────────────────────────────────────────────────────┘└─
291 exact ⟨v, by simp [hu, hv]⟩ },
id ┴ └┘ └┘
src └────┘ └┘ ┴└────┘ └┘ ┴└┘
typ └────┘ ┴└┘ ┴└────┘└┘└┘└┘┴└┘
doc └────┘ └┘ ┴└────┘ └┘ ┴└┘
txt └────┘ └┘ ┴└────┘ └┘ ┴└┘
par └────┘ └┘ ┴└────┘ └┘ ┴└┘
pid ┴ └┘ └─────┘ └┘ └┘┴
st ─────────────────┘└────────────┘└┘└┘└
292 { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
id └┘ └┘ └───────────────┘ └────┘ ┴
src └─────┘ ┴ └─────┘ └─┘ └───────────────┘└─┘ └────┘┴ └──┘ └─────────────────┘
typ └─────┘└┘┴ └─────┘└┘└─┘ └───────────────┘└─┘ └────┘┴ └──┘┴└─────────────────┘
doc └─────┘ ┴ └─────┘ └─┘ └─┘ ┴ └──┘ └─────────────────┘
txt └─────┘ ┴ └─────┘ └─┘ └─┘ ┴ └──┘ └─────────────────┘
par └─────┘ ┴ └─────┘ └─┘ └─┘ ┴ └──┘ └─────────────────┘
pid ┴ ┴ └─────┘ └─┘ └─┘ ┴ └──┘ └─────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
293 exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
id ┴ └───────────────┘ └────┘ └─┘ └─┘
src └────┘ └┘└───────────────┘└─┘ └────┘┴ └─┘ └┘
typ └────┘ ┴└┘└───────────────┘└─┘ └────┘┴└─┘└─┘└─┘└┘
doc └────┘ └┘ └─┘ ┴ └─┘ └┘
txt └────┘ └┘ └─┘ ┴ └─┘ └┘
par └────┘ └┘ └─┘ ┴ └─┘ └┘
pid ┴ └┘ └─┘ ┴ └─┘ ┴┴
st ──────────────────────────────────────────────────────┘└─
294 end)
st ────┘
295
296 lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
297 let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
id └─┘ └┘ ┴ ┴ └──────────────┘└───┘
src ┴ └──────────────┘└───┘
typ └─┘ └┘ ┴ ┴ └──────────────┘└───┘
298
299 @[simp] lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
id └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───┘ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
300 ⟨λ ⟨d, hd⟩, ⟨d * (u⁻¹ : units α), by simp [(mul_assoc _ _ _).symm, hd.symm]⟩,
id ┴┴ ┴ ┴└┘ └───┘ ┴ └───────┘
src ┴ └┘ └───┘ └────┘ └───────┘└────────────┘ ┴
typ ┴┴ ┴ ┴└┘ └───┘ ┴ └────┘ └───────┘└────────────┘└─────┘┴
doc └────┘ └────────────┘ ┴
txt └────┘ └────────────┘ ┴
par └────┘ └────────────┘ ┴
pid ┴┴ └────────────┘ ┴
st └─────────────────────────────────────┘
301 λ h, dvd.trans h (by simp)⟩
id ┴ └───────┘ ┴
src └───────┘ └──┘
typ ┴ └───────┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
302
303 lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
304 let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm
id └─┘ └┘ ┴ ┴ └──────────────┘└───┘
src ┴ └──────────────┘└───┘
typ └─┘ └┘ ┴ ┴ └──────────────┘└───┘
305
306 lemma eq_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
307 ⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
id └┘ └─┘ ┴ └┘
src └────┘ └┘ ┴
typ └┘ └─┘ ┴ └────┘└─────┘└┘└┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────┘
308 λ hb, let ⟨u, hu⟩ := h.symm in by simp [hu.symm, hb]⟩
id └┘ └─┘ ┴└───┘ └┘
src └───┘ └────┘ └┘ ┴
typ └┘ └─┘ ┴└───┘ └────┘└─────┘└┘└┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────┘
309
310 lemma ne_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
311 by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
id └───────────┘ └─────────┘ └───────────────────────┘ ┴
src └───────┘└───────────┘ └────┘└─────────┘└─┘ └───────────────────────┘┴ └─
typ └───────┘└───────────┘ └────┘└─────────┘└─┘ └───────────────────────┘┴┴└─
doc └───────┘ └────┘ └─┘ ┴ └─
txt └───────┘ └────┘ └─┘ ┴ └─
par └───────┘ └────┘ └─┘ ┴ └─
pid ┴└─┘ ┴ └─┘ ┴ ┴└
st └──────────────────────────────────────────────────────────────────────────
312
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
313 lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
id └───────────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
src └───────────┘ └┘ └───┘ └───┘
typ └───────────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ └───┘ ┴
doc └───┘ └───┘
314 ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
id └───────────────────────┘ ┴ ┴ └┘└──────┘
src └───────────────────────┘ ┴ └──────┘
typ └───────────────────────┘ ┴ ┴ └┘└──────┘
315 let ⟨u, hu⟩ := h in
id └─┘ ┴ └┘ ┴
typ └─┘ ┴ └┘ ┴
316 ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
id ┴┴ └┘└───────┘ ┴ └┘
src └───────┘ ┴ └┘ └────┘ └┘ ┴
typ ┴┴ └┘└───────┘ ┴ └┘ └────┘└─────┘└┘└─────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └──────────────────────┘
317 hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
id ┴ └──────────────┘ └───────────┘
src ┴ └────┘└──────────────┘┴ └────────┘ └────┘└───────────┘┴
typ ┴ └────┘└──────────────┘┴ └────────┘ └────┘└───────────┘┴
doc └────┘ ┴ └────────┘ └────┘ ┴
txt └────┘ ┴ └────────┘ └────┘ ┴
par └────┘ ┴ └────────┘ └────┘ ┴
pid ┴┴ ┴ └──┘ ┴ ┴
st └────────────────────────┘└──────────┘└────────────────────┘└┘
318
319 lemma prime_iff_of_associated [comm_semiring α] {p q : α}
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
320 (h : p ~ᵤ q) : prime p ↔ prime q :=
id ┴ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴
src └┘ └───┘ ┴ └───┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴
doc └───┘ └───┘
321 ⟨prime_of_associated h, prime_of_associated h.symm⟩
id └─────────────────┘ ┴ └─────────────────┘ ┴└───┘
src └─────────────────┘ └─────────────────┘ └───┘
typ └─────────────────┘ ┴ └─────────────────┘ ┴└───┘
322
323 lemma is_unit_iff_of_associated [monoid α] {a b : α} (h : a ~ᵤ b) : is_unit a ↔ is_unit b :=
id └────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └────┘ └┘ └─────┘ ┴ └─────┘
typ └────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
324 ⟨let ⟨u, hu⟩ := h in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩,
id └─┘ ┴ ┴ ┴┴ ┴ └┘
src ┴ └────┘ └┘ ┴
typ └─┘ ┴ ┴ ┴┴ ┴ └────┘└┘└┘└─────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────┘
325 let ⟨u, hu⟩ := h.symm in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩⟩
id └─┘ ┴ ┴└───┘ ┴┴ ┴ └┘
src └───┘ ┴ └────┘ └┘ ┴
typ └─┘ ┴ ┴└───┘ ┴┴ ┴ └────┘└┘└┘└─────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────┘
326
327 lemma irreducible_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q)
id └───────────┘ ┴ ┴ ┴ └┘ ┴
src └───────────┘ └┘
typ └───────────┘ ┴ ┴ ┴ └┘ ┴
328 (hp : irreducible p) : irreducible q :=
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
329 ⟨mt (is_unit_iff_of_associated h).2 hp.1,
id └┘ └───────────────────────┘ ┴ ┴ └┘┴
src └┘ └───────────────────────┘ ┴ ┴
typ └┘ └───────────────────────┘ ┴ ┴ └┘┴
330 let ⟨u, hu⟩ := h in λ a b hab,
id └─┘ ┴ ┴ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘
331 have hpab : p = a * (b * (u⁻¹ : units α)),
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴
src ┴ ┴ ┴ └┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴
332 from calc p = (p * u) * (u ⁻¹ : units α) : by simp
id ┴ ┴ ┴ ┴ └┘ └───┘ ┴
src ┴ ┴ └┘ └───┘ └────
typ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
333 ... = _ : by rw hu; simp [hab, mul_assoc],
id └┘ └─┘ └───────┘
src ─────┘ └─┘ └────┘ └┘└───────┘┴
typ ─────┘ └─┘└┘ └────┘└─┘└┘└───────┘┴
doc ─────┘ └─┘ └────┘ └┘ ┴
txt ─────┘ └─┘ └────┘ └┘ ┴
par ─────┘ └─┘ └────┘ └┘ ┴
pid ─────┘ ┴ ┴┴ └┘ ┴
st ─────┘ └───────────────────────────┘
334 (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv.symm]⟩)⟩
id └┘┴ └──┘ └──┘ └────┘ ┴┴ └────┘ ┴
src ┴ └──┘ └────┘ └────┘ ┴ └────┘ ┴
typ └┘┴ └──┘ └──┘ └────┘ ┴┴ └────┘ ┴ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────┘
335
336 lemma irreducible_iff_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) :
id └───────────┘ ┴ ┴ ┴ └┘ ┴
src └───────────┘ └┘
typ └───────────┘ ┴ ┴ ┴ └┘ ┴
337 irreducible p ↔ irreducible q :=
id └─────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
338 ⟨irreducible_of_associated h, irreducible_of_associated h.symm⟩
id └───────────────────────┘ ┴ └───────────────────────┘ ┴└───┘
src └───────────────────────┘ └───────────────────────┘ └───┘
typ └───────────────────────┘ ┴ └───────────────────────┘ ┴└───┘
339
340 lemma associated_mul_left_cancel [integral_domain α] {a b c d : α}
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
341 (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
342 let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
id └─┘ ┴ ┴ └─┘ ┴ └─────────────┘ └┘
src └─────────────┘
typ └─┘ ┴ ┴ └─┘ ┴ └─────────────┘ └┘
343 ⟨u * (v : units α), (domain.mul_left_inj ha).1
id ┴ └───┘ ┴ └─────────────────┘ └┘ ┴
src ┴ └───┘ └─────────────────┘ ┴
typ ┴ └───┘ ┴ └─────────────────┘ └┘ ┴
doc └─────────────────┘
344 begin
st └─────
345 rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu],
id └┘ └───────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ └┘
src └────┘ └┘└───────┘┴ ┴ └─┘ └┘ └┘└───────────┘┴ └──┘ ┴
typ └────┘└┘└┘└───────┘┴┴┴ ┴└─┘┴└┘┴└┘└───────────┘┴┴└──┘└┘┴
doc └────┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └──┘ ┴
txt └────┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └──┘ ┴
par └────┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └──┘ ┴
pid └──┘ └┘ ┴ ┴ └─┘ └┘ └┘ ┴ └──┘ ┴
st ───────────┘└─────────────────────┘└───────────────┘└────┘└──
346 simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
id └───────┘ └──────┘ └───────────┘
src └────┘ └┘└───────┘└┘└──────┘└┘└───────────┘└─
typ └────┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st ───────────────────────────────────────────────────────
347 end⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
348
349 lemma associated_mul_right_cancel [integral_domain α] {a b c d : α} :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
350 a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
351 by rw [mul_comm a, mul_comm c]; exact associated_mul_left_cancel
id └──────┘ ┴ └──────┘ ┴ └────────────────────────┘
src └──┘└──────┘┴ └┘└──────┘┴ ┴ └────┘└────────────────────────┘└
typ └──┘└──────┘┴┴└┘└──────┘┴┴┴ └────┘└────────────────────────┘└
doc └──┘ ┴ └┘ ┴ ┴ └────┘ └
txt └──┘ ┴ └┘ ┴ ┴ └────┘ └
par └──┘ ┴ └┘ ┴ ┴ └────┘ └
pid └┘ ┴ └┘ ┴ ┴ ┴ └
st └─────────────┘└──────────┘┴└──────────────────────────────────
352
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
353 def associates (α : Type*) [monoid α] : Type* :=
id └────┘ ┴
src └────┘
typ └────┘ ┴
354 quotient (associated.setoid α)
id └──────┘ └───────────────┘ ┴
src └──────┘ └───────────────┘
typ └──────┘ └───────────────┘ ┴
355
356 namespace associates
357 open associated
358
359 protected def mk {α : Type*} [monoid α] (a : α) : associates α :=
id └────┘ ┴ ┴ └────────┘ ┴
src └────┘ └────────┘
typ └────┘ ┴ ┴ └────────┘ ┴
360 ⟦ a ⟧
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
361
362 instance [monoid α] : inhabited (associates α) := ⟨⟦1⟧⟩
id └────┘ ┴ └───────┘ └────────┘ ┴ ┴ ┴
src └────┘ └───────┘ └────────┘ ┴ ┴
typ └────┘ ┴ └───────┘ └────────┘ ┴ ┴ ┴
363
364 theorem mk_eq_mk_iff_associated [monoid α] {a b : α} :
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
365 associates.mk a = associates.mk b ↔ a ~ᵤ b :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴
src └───────────┘ ┴ └───────────┘ ┴ └┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴
366 iff.intro quotient.exact quot.sound
id └───────┘ └────────────┘ └────────┘
src └───────┘ └────────────┘ └────────┘
typ └───────┘ └────────────┘ └────────┘
367
368 theorem quotient_mk_eq_mk [monoid α] (a : α) : ⟦ a ⟧ = associates.mk a := rfl
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘
src └────┘ ┴ ┴ ┴ └───────────┘ └─┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘
369
370 theorem quot_mk_eq_mk [monoid α] (a : α) : quot.mk setoid.r a = associates.mk a := rfl
id └────┘ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └───────────┘ ┴ └─┘
src └────┘ └──────┘ ┴ └───────────┘ └─┘
typ └────┘ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └───────────┘ ┴ └─┘
371
372 theorem forall_associated [monoid α] {p : associates α → Prop} :
id └────┘ ┴ └────────┘ ┴
src └────┘ └────────┘
typ └────┘ ┴ └────────┘ ┴
373 (∀a, p a) ↔ (∀a, p (associates.mk a)) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
src ┴ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
374 iff.intro
id └───────┘
src └───────┘
typ └───────┘
375 (assume h a, h _)
id ┴ ┴ ┴
typ ┴ ┴ ┴
376 (assume h a, quotient.induction_on a h)
id ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘
typ ┴ ┴ └───────────────────┘ ┴ ┴
377
378 instance [monoid α] : has_one (associates α) := ⟨⟦ 1 ⟧⟩
id └────┘ ┴ └─────┘ └────────┘ ┴ ┴ ┴
src └────┘ └─────┘ └────────┘ ┴ ┴
typ └────┘ ┴ └─────┘ └────────┘ ┴ ┴ ┴
379
380 theorem one_eq_mk_one [monoid α] : (1 : associates α) = associates.mk 1 := rfl
id └────┘ ┴ └────────┘ ┴ ┴ └───────────┘ └─┘
src └────┘ └────────┘ ┴ └───────────┘ └─┘
typ └────┘ ┴ └────────┘ ┴ ┴ └───────────┘ └─┘
381
382 instance [monoid α] : has_bot (associates α) := ⟨1⟩
id └────┘ ┴ └─────┘ └────────┘ ┴
src └────┘ └─────┘ └────────┘
typ └────┘ ┴ └─────┘ └────────┘ ┴
doc └─────┘
383
384 section comm_monoid
385 variable [comm_monoid α]
id └─────────┘
src └─────────┘
typ └─────────┘
386
387 instance : has_mul (associates α) :=
id └─────┘ └────────┘ ┴
src └─────┘ └────────┘
typ └─────┘ └────────┘ ┴
388 ⟨λa' b', quotient.lift_on₂ a' b' (λa b, ⟦ a * b ⟧) $
id └┘ └┘ └───────────────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ ┴ ┴
typ └┘ └┘ └───────────────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
389 assume a₁ a₂ b₁ b₂ ⟨c₁, h₁⟩ ⟨c₂, h₂⟩,
id └┘ └┘ └┘ └┘ ┴└┘ ┴└┘
typ └┘ └┘ └┘ └┘ ┴└┘ ┴└┘
390 quotient.sound $ ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩⟩
id └────────────┘ ┴ └───────┘ └──────┘ └───────────┘
src └────────────┘ ┴ └────┘ └┘ └┘└───────┘└┘└──────┘└┘└───────────┘┴
typ └────────────┘ ┴ └────┘└─────┘└┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────┘
391
392 theorem mk_mul_mk {x y : α} : associates.mk x * associates.mk y = associates.mk (x * y) :=
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
393 rfl
id └─┘
src └─┘
typ └─┘
394
395 instance : comm_monoid (associates α) :=
id └─────────┘ └────────┘ ┴
src └─────────┘ └────────┘
typ └─────────┘ └────────┘ ┴
396 { one := 1,
397 mul := (*),
id ┴
src ┴
typ ┴
398 mul_one := assume a', quotient.induction_on a' $
id └┘ └───────────────────┘ └┘
src └───────────────────┘
typ └┘ └───────────────────┘ └┘
399 assume a, show ⟦a * 1⟧ = ⟦ a ⟧, by simp,
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
400 one_mul := assume a', quotient.induction_on a' $
id └┘ └───────────────────┘ └┘
src └───────────────────┘
typ └┘ └───────────────────┘ └┘
401 assume a, show ⟦1 * a⟧ = ⟦ a ⟧, by simp,
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
402 mul_assoc := assume a' b' c', quotient.induction_on₃ a' b' c' $
id └┘ └┘ └┘ └────────────────────┘ └┘ └┘ └┘
src └────────────────────┘
typ └┘ └┘ └┘ └────────────────────┘ └┘ └┘ └┘
403 assume a b c, show ⟦a * b * c⟧ = ⟦a * (b * c)⟧, by rw [mul_assoc],
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └────────────┘┴
404 mul_comm := assume a' b', quotient.induction_on₂ a' b' $
id └┘ └┘ └────────────────────┘ └┘ └┘
src └────────────────────┘
typ └┘ └┘ └────────────────────┘ └┘ └┘
405 assume a b, show ⟦a * b⟧ = ⟦b * a⟧, by rw [mul_comm] }
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └──────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└──────┘└┘
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ └──┘└──────┘└┘
doc └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st └───────────┘┴┴
406
407 instance : preorder (associates α) :=
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
408 { le := λa b, ∃c, a * c = b,
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
409 le_refl := assume a, ⟨1, by simp⟩,
id ┴
src └──┘
typ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
410 le_trans := assume a b c ⟨f₁, h₁⟩ ⟨f₂, h₂⟩, ⟨f₁ * f₂, h₂ ▸ h₁ ▸ (mul_assoc _ _ _).symm⟩}
id ┴ ┴ ┴ ┴└┘ └┘ ┴└┘ └┘ ┴ ┴ ┴ └───────┘ └──┘
src ┴ ┴ ┴ └───────┘ └──┘
typ ┴ ┴ ┴ ┴└┘ └┘ ┴└┘ └┘ ┴ ┴ ┴ └───────┘ └──┘
411
412 instance : has_dvd (associates α) := ⟨(≤)⟩
id └─────┘ └────────┘ ┴ ┴
src └─────┘ └────────┘ ┴
typ └─────┘ └────────┘ ┴ ┴
413
414 @[simp] lemma mk_one : associates.mk (1 : α) = 1 := rfl
id └───────────┘ ┴ ┴ └─┘
src └───────────┘ ┴ └─┘
typ └───────────┘ ┴ ┴ └─┘
doc └──┘
415
416 lemma mk_pow (a : α) (n : ℕ) : associates.mk (a ^ n) = (associates.mk a) ^ n :=
id ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
typ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
417 by induction n; simp [*, pow_succ, associates.mk_mul_mk.symm]
id ┴ └──────┘
src └────────┘ └───────┘└──────┘└┘ └─
typ └────────┘┴ └───────┘└──────┘└┘└───────────────────────┘└─
doc └────────┘ └───────┘ └┘ └─
txt └────────┘ └───────┘ └┘ └─
par └────────┘ └───────┘ └┘ └─
pid ┴ ┴└──┘ └┘ ┴└
st └───────────────────────────────────────────────────────────
418
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
419 lemma dvd_eq_le : ((∣) : associates α → associates α → Prop) = (≤) := rfl
id ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘
src ┴ └────────┘ └────────┘ ┴ ┴ └─┘
typ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ └─┘
420
421 theorem prod_mk {p : multiset α} : (p.map associates.mk).prod = associates.mk p.prod :=
id └──────┘ ┴ ┴└──┘ └───────────┘ └──┘ ┴ └───────────┘ ┴└───┘
src └──────┘ └──┘ └───────────┘ └──┘ ┴ └───────────┘ └───┘
typ └──────┘ ┴ ┴└──┘ └───────────┘ └──┘ ┴ └───────────┘ ┴└───┘
doc └──────┘ └──┘ └──┘ └───┘
422 multiset.induction_on p (by simp; refl) $ assume a s ih, by simp [ih]; refl
id └───────────────────┘ ┴ ┴ ┴ └┘ └┘
src └───────────────────┘ └──┘ └──┘ └────┘ ┴ └────
typ └───────────────────┘ ┴ └──┘ └──┘ ┴ ┴ └┘ └────┘└┘┴ └────
doc └──┘ └──┘ └────┘ ┴ └────
txt └──┘ └──┘ └────┘ ┴ └────
par └──┘ └──┘ └────┘ ┴ └────
pid ┴┴ ┴ └
st └─────────┘ └────────────────
423
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
424 theorem rel_associated_iff_map_eq_map {p q : multiset α} :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
425 multiset.rel associated p q ↔ p.map associates.mk = q.map associates.mk :=
id └──────────┘ └────────┘ ┴ ┴ ┴ ┴└──┘ └───────────┘ ┴ ┴└──┘ └───────────┘
src └──────────┘ └────────┘ ┴ └──┘ └───────────┘ ┴ └──┘ └───────────┘
typ └──────────┘ └────────┘ ┴ ┴ ┴ ┴└──┘ └───────────┘ ┴ ┴└──┘ └───────────┘
doc └──────────┘ └──┘ └──┘
426 by rw [← multiset.rel_eq];
id └─────────────┘
src └────┘└─────────────┘┴
typ └────┘└─────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st └────────────────────┘┴└─
427 simp [multiset.rel_map_left, multiset.rel_map_right, mk_eq_mk_iff_associated]
id └───────────────────┘ └────────────────────┘ └─────────────────────┘
src └────┘└───────────────────┘└┘└────────────────────┘└┘└─────────────────────┘└─
typ └────┘└───────────────────┘└┘└────────────────────┘└┘└─────────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ────────────────────────────────────────────────────────────────────────────────
428
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
429 theorem mul_eq_one_iff {x y : associates α} : x * y = 1 ↔ (x = 1 ∧ y = 1) :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
430 iff.intro
id └───────┘
src └───────┘
typ └───────┘
431 (quotient.induction_on₂ x y $ assume a b h,
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
432 have a * b ~ᵤ 1, from quotient.exact h,
id ┴ ┴ ┴ └┘ └────────────┘ ┴
src ┴ └┘ └────────────┘
typ ┴ ┴ ┴ └┘ └────────────┘ ┴
433 ⟨quotient.sound $ associated_one_of_associated_mul_one this,
id └────────────┘ └──────────────────────────────────┘ └──┘
src └────────────┘ └──────────────────────────────────┘
typ └────────────┘ └──────────────────────────────────┘ └──┘
434 quotient.sound $ associated_one_of_associated_mul_one $ by rwa [mul_comm] at this⟩)
id └────────────┘ └──────────────────────────────────┘ └──────┘
src └────────────┘ └──────────────────────────────────┘ └───┘└──────┘└───────┘
typ └────────────┘ └──────────────────────────────────┘ └───┘└──────┘└───────┘
doc └───┘ └───────┘
txt └───┘ └───────┘
par └───┘ └───────┘
pid └┘ ┴└──────┘
st └────────────┘┴└──────┘
435 (by simp {contextual := tt})
id └┘
src └───┘ └────────────┘└┘┴
typ └───┘ └────────────┘└┘┴
doc └───┘ └────────────┘ ┴
txt └───┘ └────────────┘ ┴
par └───┘ └────────────┘ ┴
pid ┴ └────────────┘ ┴
st └──────────────────────┘
436
437 theorem prod_eq_one_iff {p : multiset (associates α)} :
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
doc └──────┘
438 p.prod = 1 ↔ (∀a ∈ p, (a:associates α) = 1) :=
id ┴└───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └───┘ ┴ ┴ └────────┘ ┴
typ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └───┘
439 multiset.induction_on p
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
440 (by simp)
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
441 (by simp [mul_eq_one_iff, or_imp_distrib, forall_and_distrib] {contextual := tt})
id └────────────┘ └────────────┘ └────────────────┘ └┘
src └────┘└────────────┘└┘└────────────┘└┘└────────────────┘└┘ └────────────┘└┘┴
typ └────┘└────────────┘└┘└────────────┘└┘└────────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ └┘ ┴┴ └────────────┘ ┴
st └───────────────────────────────────────────────────────────────────────────┘
442
443 theorem coe_unit_eq_one : ∀u:units (associates α), (u : associates α) = 1
id ┴ └───┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴
src └───┘ └────────┘ └────────┘ ┴
typ ┴ └───┘ └────────┘ ┴ ┴ └────────┘ ┴ ┴
444 | ⟨u, v, huv, hvu⟩ := by rw [mul_eq_one_iff] at huv; exact huv.1
id └────────────┘ └─┘
src └──┘└────────────┘└──────┘ └────┘ └──
typ └──┘└────────────┘└──────┘ └────┘└─┘└──
doc └──┘ └──────┘ └────┘ └──
txt └──┘ └──────┘ └────┘ └──
par └──┘ └──────┘ └────┘ └──
pid └┘ ┴└─────┘ ┴ └──
st └─────────────────┘┴└────────────────────
445
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
446 theorem is_unit_iff_eq_one (a : associates α) : is_unit a ↔ a = 1 :=
id └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────────┘ └─────┘ ┴ ┴
typ └────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
447 iff.intro
id └───────┘
src └───────┘
typ └───────┘
448 (assume ⟨u, h⟩, h.symm ▸ coe_unit_eq_one _)
id ┴ ┴ └───┘ ┴ └─────────────┘
src └───┘ ┴ └─────────────┘
typ ┴ ┴ └───┘ ┴ └─────────────┘
449 (assume h, h.symm ▸ is_unit_one)
id ┴ ┴└───┘ ┴ └─────────┘
src └───┘ ┴ └─────────┘
typ ┴ ┴└───┘ ┴ └─────────┘
450
451 theorem is_unit_mk {a : α} : is_unit (associates.mk a) ↔ is_unit a :=
id ┴ └─────┘ └───────────┘ ┴ ┴ └─────┘ ┴
src └─────┘ └───────────┘ ┴ └─────┘
typ ┴ └─────┘ └───────────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
452 calc is_unit (associates.mk a) ↔ a ~ᵤ 1 :
id └─────┘ └───────────┘ ┴ ┴ └┘
src └─────┘ └───────────┘ └┘
typ └─────┘ └───────────┘ ┴ ┴ └┘
doc └─────┘
453 by rw [is_unit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
id └────────────────┘ └───────────┘ └─────────────────────┘
src └──┘└────────────────┘└┘└───────────┘└┘└─────────────────────┘└─
typ └──┘└────────────────┘└┘└───────────┘└┘└─────────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────────────────┘└─────────────┘└───────────────────────┘┴└
454 ... ↔ is_unit a : associated_one_iff_is_unit
id └─────┘ ┴ └────────────────────────┘
src ─┘ └─────┘ └────────────────────────┘
typ ─┘ └─────┘ ┴ └────────────────────────┘
doc ─┘ └─────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
455
456 section order
457
458 theorem mul_mono {a b c d : associates α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
459 a * c ≤ b * d :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
460 let ⟨x, hx⟩ := h₁, ⟨y, hy⟩ := h₂ in
id └─┘ ┴ └┘ ┴ └┘
typ └─┘ ┴ └┘ ┴ └┘
461 ⟨x * y, by simp [hx.symm, hy.symm, mul_comm, mul_assoc, mul_left_comm]⟩
id ┴ └──────┘ └───────┘ └───────────┘
src ┴ └────┘ └┘ └┘└──────┘└┘└───────┘└┘└───────────┘┴
typ ┴ └────┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────┘
462
463 theorem one_le {a : associates α} : 1 ≤ a :=
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
464 ⟨a, one_mul a⟩
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
465
466 theorem prod_le_prod {p q : multiset (associates α)} (h : p ≤ q) : p.prod ≤ q.prod :=
id └──────┘ └────────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
src └──────┘ └────────┘ ┴ └───┘ ┴ └───┘
typ └──────┘ └────────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴└───┘
doc └──────┘ └───┘ └───┘
467 begin
st └─────
468 haveI := classical.dec_eq (associates α),
id └──────────────┘ └────────┘ ┴
src └───────┘└──────────────┘┴ └────────┘┴ ┴
typ └───────┘└──────────────┘┴ └────────┘┴┴┴
doc └───────┘ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴
pid ┴└─┘ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
469 haveI := classical.dec_eq α,
id └──────────────┘ ┴
src └───────┘└──────────────┘┴
typ └───────┘└──────────────┘┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st ────────────────────────────┘└─
470 suffices : p.prod ≤ (p + (q - p)).prod, { rwa [multiset.add_sub_of_le h] at this },
id └────┘ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴
src └─────────┘└────┘┴┴┴ ┴┴┴ ┴┴┴ └─────┘ └───┘└────────────────────┘┴ └────────┘
typ └─────────┘└────┘┴┴┴ ┴┴┴ ┴┴┴┴┴└─────┘ └───┘└────────────────────┘┴┴└────────┘
doc └─────────┘└────┘┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └───┘ ┴ └────────┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └───┘ ┴ └────────┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └───┘ ┴ └────────┘
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ └┘ ┴ ┴└──────┘┴
st ───────────────────────────────────────┘└──┘└───────────────────────────┘┴└───────┘└┘└
471 suffices : p.prod * 1 ≤ p.prod * (q - p).prod, { simpa },
id ┴ └────┘ ┴ ┴
src └─────────┘ ┴┴└─┘ ┴└────┘┴ ┴ ┴ ┴ └────┘ └────┘
typ └─────────┘ ┴┴└─┘ ┴└────┘┴ ┴ ┴┴ ┴┴└────┘ └────┘
doc └─────────┘ ┴ └─┘ ┴└────┘┴ ┴ ┴ ┴ └────┘ └────┘
txt └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘
par └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘
pid └───────┘└┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───┘┴ ┴
st ──────────────────────────────────────────────┘└──┘└────┘└┘└
472 exact mul_mono (le_refl p.prod) one_le
id └──────┘ └─────┘ └────┘ └────┘
src └────┘└──────┘┴ └─────┘┴└────┘└┘└────┘┴
typ └────┘└──────┘┴ └─────┘┴└────┘└┘└────┘┴
doc └────┘ ┴ ┴└────┘└┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────┘
473 end
st └─┘
474
475 theorem le_mul_right {a b : associates α} : a ≤ a * b := ⟨b, rfl⟩
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └────────┘ ┴ ┴ └─┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
476
477 theorem le_mul_left {a b : associates α} : a ≤ b * a :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
478 by rw [mul_comm]; exact le_mul_right
id └──────┘ └──────────┘
src └──┘└──────┘┴ └────┘└──────────┘└
typ └──┘└──────┘┴ └────┘└──────────┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └───────────┘┴└────────────────────
479
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
480 end order
481
482 end comm_monoid
483
484 instance [has_zero α] [monoid α] : has_zero (associates α) := ⟨⟦ 0 ⟧⟩
id └──────┘ ┴ └────┘ ┴ └──────┘ └────────┘ ┴ ┴ ┴
src └──────┘ └────┘ └──────┘ └────────┘ ┴ ┴
typ └──────┘ ┴ └────┘ ┴ └──────┘ └────────┘ ┴ ┴ ┴
485 instance [has_zero α] [monoid α] : has_top (associates α) := ⟨0⟩
id └──────┘ ┴ └────┘ ┴ └─────┘ └────────┘ ┴
src └──────┘ └────┘ └─────┘ └────────┘
typ └──────┘ ┴ └────┘ ┴ └─────┘ └────────┘ ┴
doc └─────┘
486
487 section comm_semiring
488 variables [comm_semiring α]
id └───────────┘
src └───────────┘
typ └───────────┘
489
490 @[simp] theorem mk_zero_eq (a : α) : associates.mk a = 0 ↔ a = 0 :=
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
491 ⟨assume h, (associated_zero_iff_eq_zero a).1 $ quotient.exact h, assume h, h.symm ▸ rfl⟩
id ┴ └─────────────────────────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴└───┘ ┴ └─┘
src └─────────────────────────┘ ┴ └────────────┘ └───┘ ┴ └─┘
typ ┴ └─────────────────────────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴└───┘ ┴ └─┘
492
493 @[simp] theorem mul_zero : ∀(a : associates α), a * 0 = 0 :=
id └────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴
doc └──┘
494 by rintros ⟨a⟩; show associates.mk (a * 0) = associates.mk 0; rw [mul_zero]
id ┴ ┴ ┴ └───────────┘ └──────┘
src └─────────┘ └───┘ ┴ ┴┴└──┘┴┴└───────────┘└┘ └──┘└──────┘└─
typ └─────────┘ └───┘ ┴ ┴┴┴└──┘┴┴└───────────┘└┘ └──┘└──────┘└─
doc └─────────┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └──┘ └─
txt └─────────┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └──┘ └─
par └─────────┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └──┘ └─
pid └──┘ └───┘ ┴ ┴ └──┘ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────────────────────────────────────┘└──────┘┴└
495
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
496 @[simp] protected theorem zero_mul : ∀(a : associates α), 0 * a = 0 :=
id └────────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴
doc └──┘
497 by rintros ⟨a⟩; show associates.mk (0 * a) = associates.mk 0; rw [zero_mul]
id ┴ ┴ ┴ └───────────┘ └──────┘
src └─────────┘ └───┘ ┴ └┘┴┴ └┘┴┴└───────────┘└┘ └──┘└──────┘└─
typ └─────────┘ └───┘ ┴ └┘┴┴┴└┘┴┴└───────────┘└┘ └──┘└──────┘└─
doc └─────────┘ └───┘ ┴ └┘ ┴ └┘ ┴ └┘ └──┘ └─
txt └─────────┘ └───┘ ┴ └┘ ┴ └┘ ┴ └┘ └──┘ └─
par └─────────┘ └───┘ ┴ └┘ ┴ └┘ ┴ └┘ └──┘ └─
pid └──┘ └───┘ ┴ └┘ ┴ └┘ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────────────────────────────────────┘└──────┘┴└
498
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
499 theorem mk_eq_zero_iff_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
500 calc associates.mk a = 0 ↔ (a ~ᵤ 0) : mk_eq_mk_iff_associated
id └───────────┘ ┴ ┴ ┴ └┘ └─────────────────────┘
src └───────────┘ ┴ └┘ └─────────────────────┘
typ └───────────┘ ┴ ┴ ┴ └┘ └─────────────────────┘
501 ... ↔ a = 0 : associated_zero_iff_eq_zero a
id ┴ ┴ └─────────────────────────┘ ┴
src ┴ └─────────────────────────┘
typ ┴ ┴ └─────────────────────────┘ ┴
502
503 theorem dvd_of_mk_le_mk {a b : α} : associates.mk a ≤ associates.mk b → a ∣ b
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ └───────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
504 | ⟨c', hc'⟩ := (quotient.induction_on c' $ assume c hc,
id └┘ └─┘ └───────────────────┘ ┴ └┘
src └───────────────────┘
typ └┘ └─┘ └───────────────────┘ ┴ └┘
505 let ⟨d, hd⟩ := (quotient.exact hc).symm in
id └─┘ ┴ └────────────┘ └┘ └──┘
src └────────────┘ └──┘
typ └─┘ ┴ └────────────┘ └┘ └──┘
506 ⟨(↑d⁻¹) * c,
id ┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴
507 calc b = (a * c) * ↑d⁻¹ : by rw [← hd, mul_assoc, units.mul_inv, mul_one]
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └───────┘ └───────────┘ └─────┘
src ┴ ┴ ┴ └┘ └────┘ └┘└───────┘└┘└───────────┘└┘└─────┘└─
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────┘└┘└┘└───────┘└┘└───────────┘└┘└─────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ ┴└
st └───────┘└─────────┘└─────────────┘└───────┘┴└
508 ... = a * (↑d⁻¹ * c) : by ac_refl⟩) hc'
id ┴ ┴ ┴ └┘ ┴ ┴
src ───────┘ ┴ ┴ └┘ ┴ └─────┘
typ ───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────┘
doc ───────┘ └─────┘
txt ───────┘ └─────┘
par ───────┘ └─────┘
pid ───────┘
st ───────┘ └──────┘
509
510 theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → associates.mk a ≤ associates.mk b :=
id ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
src ┴ └───────────┘ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
511 assume ⟨c, hc⟩, ⟨associates.mk c, by simp [hc]; refl⟩
id ┴┴ └───────────┘ └┘
src └───────────┘ └────┘ ┴ └──┘
typ ┴┴ └───────────┘ └────┘└┘┴ └──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴┴ ┴
st └──────────────┘
512
513 theorem mk_le_mk_iff_dvd_iff {a b : α} : associates.mk a ≤ associates.mk b ↔ a ∣ b :=
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ └───────────┘ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
514 iff.intro dvd_of_mk_le_mk mk_le_mk_of_dvd
id └───────┘ └─────────────┘ └─────────────┘
src └───────┘ └─────────────┘ └─────────────┘
typ └───────┘ └─────────────┘ └─────────────┘
515
516 def prime (p : associates α) : Prop := p ≠ 0 ∧ p ≠ 1 ∧ (∀a b, p ≤ a * b → p ≤ a ∨ p ≤ b)
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
517
518 lemma prime.ne_zero {p : associates α} (hp : prime p) : p ≠ 0 :=
id └────────┘ ┴ └───┘ ┴ ┴ ┴
src └────────┘ └───┘ ┴
typ └────────┘ ┴ └───┘ ┴ ┴ ┴
519 hp.1
id └┘┴
src ┴
typ └┘┴
520
521 lemma prime.ne_one {p : associates α} (hp : prime p) : p ≠ 1 :=
id └────────┘ ┴ └───┘ ┴ ┴ ┴
src └────────┘ └───┘ ┴
typ └────────┘ ┴ └───┘ ┴ ┴ ┴
522 hp.2.1
id └┘┴ ┴
src ┴ ┴
typ └┘┴ ┴
523
524 lemma prime.le_or_le {p : associates α} (hp : prime p) {a b : associates α} (h : p ≤ a * b) :
id └────────┘ ┴ └───┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘ └────────┘ ┴ ┴
typ └────────┘ ┴ └───┘ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
525 p ≤ a ∨ p ≤ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
526 hp.2.2 a b h
id └┘┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴
527
528 lemma exists_mem_multiset_le_of_prime {s : multiset (associates α)} {p : associates α}
id └──────┘ └────────┘ ┴ └────────┘ ┴
src └──────┘ └────────┘ └────────┘
typ └──────┘ └────────┘ ┴ └────────┘ ┴
doc └──────┘
529 (hp : prime p) :
id └───┘ ┴
src └───┘
typ └───┘ ┴
530 p ≤ s.prod → ∃a∈s, p ≤ a :=
id ┴ ┴ ┴└───┘ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴└───┘ ┴┴ ┴┴ ┴ ┴ ┴
doc └───┘
531 multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq).1).elim) $
id └───────────────────┘ ┴ ┴ └┘ └┘└─────┘ └────────────┘┴ ┴ └──┘
src └───────────────────┘ └┘ └─────┘ └────────────┘┴ ┴ └──┘
typ └───────────────────┘ ┴ ┴ └┘ └┘└─────┘ └────────────┘┴ ┴ └──┘
532 assume a s ih h,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
533 have p ≤ a * s.prod, by simpa using h,
id ┴ ┴ ┴ ┴ ┴└───┘ ┴
src ┴ ┴ └───┘ └──────────┘
typ ┴ ┴ ┴ ┴ ┴└───┘ └──────────┘┴
doc └───┘ └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────┘
534 match hp.le_or_le this with
id └┘└───────┘ └──┘
src └───────┘
typ └┘└───────┘ └──┘
535 | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
id └────┘ ┴ ┴ └────────────────────┘ ┴ ┴
src └────┘ └────────────────────┘
typ └────┘ ┴ ┴ └────────────────────┘ ┴ ┴
536 | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
id └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘ └──────────────────────┘
src └────┘ └──────────────────────┘
typ └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘ └──────────────────────┘
537 end
538
539 lemma prime_mk (p : α) : prime (associates.mk p) ↔ _root_.prime p :=
id ┴ └───┘ └───────────┘ ┴ ┴ └──────────┘ ┴
src └───┘ └───────────┘ ┴ └──────────┘
typ ┴ └───┘ └───────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘
540 begin
st └─────
541 rw [associates.prime, _root_.prime, forall_associated],
id └──────────────┘ └──────────┘ └───────────────┘
src └──┘└──────────────┘└┘└──────────┘└┘└───────────────┘┴
typ └──┘└──────────────┘└┘└──────────┘└┘└───────────────┘┴
doc └──┘ └┘└──────────┘└┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────────────────────┘└────────────┘└─────────────────┘└──
542 transitivity,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
st ─────────────┘└─
543 { apply and_congr, refl,
id └───────┘
src └────┘└───────┘ └──┘
typ └────┘└───────┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st ───┘└─────────────┘└────┘└─
544 apply and_congr, refl,
id └───────┘
src └────┘└───────┘ └──┘
typ └────┘└───────┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st ──────────────────┘└────┘└─
545 apply forall_congr, assume a,
id └──────────┘
src └────┘└──────────┘ └──────┘
typ └────┘└──────────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ─────────────────────┘└────────┘└─
546 exact forall_associated },
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘└┘└
547 apply and_congr,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
548 { rw [(≠), mk_zero_eq] },
id ┴ └────────┘
src └──┘┴└──┘└────────┘└┘
typ └──┘┴└──┘└────────┘└┘
doc └──┘ └──┘ └┘
txt └──┘ └──┘ └┘
par └──┘ └──┘ └┘
pid └┘ └──┘ ┴┴
st ───┘└─────┘└──────────┘┴┴└┘└
549 apply and_congr,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
550 { rw [(≠), ← is_unit_iff_eq_one, is_unit_mk], },
id ┴ └────────────────┘ └────────┘
src └──┘┴└────┘└────────────────┘└┘└────────┘┴
typ └──┘┴└────┘└────────────────┘└┘└────────┘┴
doc └──┘ └────┘ └┘ ┴
txt └──┘ └────┘ └┘ ┴
par └──┘ └────┘ └┘ ┴
pid └┘ └────┘ └┘ ┴
st ───┘└─────┘└────────────────────┘└──────────┘└───┘└
551 apply forall_congr, assume a,
id └──────────┘
src └────┘└──────────┘ └──────┘
typ └────┘└──────────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ───────────────────┘└────────┘└─
552 apply forall_congr, assume b,
id └──────────┘
src └────┘└──────────┘ └──────┘
typ └────┘└──────────┘ └──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ───────────────────┘└────────┘└─
553 rw [mk_mul_mk, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff]
id └───────┘ └──────────────────┘ └──────────────────┘ └──────────────────┘
src └──┘└───────┘└┘└──────────────────┘└┘└──────────────────┘└┘└──────────────────┘└┘
typ └──┘└───────┘└┘└──────────────────┘└┘└──────────────────┘└┘└──────────────────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ──────────────┘└────────────────────┘└────────────────────┘└────────────────────┘┴┴
554 end
st └─┘
555
556 end comm_semiring
557
558 section integral_domain
559 variable [integral_domain α]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
560
561 instance : partial_order (associates α) :=
id └───────────┘ └────────┘ ┴
src └───────────┘ └────────┘
typ └───────────┘ └────────┘ ┴
562 { le_antisymm := assume a' b',
id └┘ └┘
typ └┘ └┘
563 quotient.induction_on₂ a' b' $ assume a b ⟨f₁', h₁⟩ ⟨f₂', h₂⟩,
id └────────────────────┘ └┘ └┘ ┴ ┴ ┴└─┘ └┘ ┴└─┘ └┘
src └────────────────────┘
typ └────────────────────┘ └┘ └┘ ┴ ┴ ┴└─┘ └┘ ┴└─┘ └┘
564 (quotient.induction_on₂ f₁' f₂' $ assume f₁ f₂ h₁ h₂,
id └────────────────────┘ └┘ └┘ └┘ └┘
src └────────────────────┘
typ └────────────────────┘ └┘ └┘ └┘ └┘
565 let ⟨c₁, h₁⟩ := quotient.exact h₁, ⟨c₂, h₂⟩ := quotient.exact h₂ in
id └─┘ └┘ └────────────┘ └┘ └┘ └────────────┘ └┘
src └────────────┘ └────────────┘
typ └─┘ └┘ └────────────┘ └┘ └┘ └────────────┘ └┘
566 quotient.sound $ associated_of_dvd_dvd
id └────────────┘ └───────────────────┘
src └────────────┘ └───────────────────┘
typ └────────────┘ └───────────────────┘
567 (h₁ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
id ┴ └─────────────────┘ └───────────┘
src ┴ └─────────────────┘ └───────────┘
typ ┴ └─────────────────┘ └───────────┘
568 (h₂ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)) h₁ h₂
id ┴ └─────────────────┘ └───────────┘
src ┴ └─────────────────┘ └───────────┘
typ ┴ └─────────────────┘ └───────────┘
569 .. associates.preorder }
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
570
571 instance : lattice.order_bot (associates α) :=
id └───────────────┘ └────────┘ ┴
src └───────────────┘ └────────┘
typ └───────────────┘ └────────┘ ┴
doc └───────────────┘
572 { bot := 1,
573 bot_le := assume a, one_le,
id ┴ └────┘
src └────┘
typ ┴ └────┘
574 .. associates.partial_order }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
575
576 instance : lattice.order_top (associates α) :=
id └───────────────┘ └────────┘ ┴
src └───────────────┘ └────────┘
typ └───────────────┘ └────────┘ ┴
doc └───────────────┘
577 { top := 0,
578 le_top := assume a, ⟨0, mul_zero a⟩,
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
579 .. associates.partial_order }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
580
581 theorem zero_ne_one : (0 : associates α) ≠ 1 :=
id └────────┘ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴
582 assume h,
id ┴
typ ┴
583 have (0 : α) ~ᵤ 1, from quotient.exact h,
id ┴ └┘ └────────────┘ ┴
src └┘ └────────────┘
typ ┴ └┘ └────────────┘ ┴
584 have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
id ┴ ┴ └─────────────────────────┘ ┴ └──┘└───┘ └──┘
src ┴ └─────────────────────────┘ ┴ └───┘ └──┘
typ ┴ ┴ └─────────────────────────┘ ┴ └──┘└───┘ └──┘
585 zero_ne_one this
id └─────────┘ └──┘
src └─────────┘
typ └─────────┘ └──┘
586
587 theorem mul_eq_zero_iff {x y : associates α} : x * y = 0 ↔ x = 0 ∨ y = 0 :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
588 iff.intro
id └───────┘
src └───────┘
typ └───────┘
589 (quotient.induction_on₂ x y $ assume a b h,
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
590 have a * b = 0, from (associated_zero_iff_eq_zero _).1 (quotient.exact h),
id ┴ ┴ ┴ ┴ └─────────────────────────┘ ┴ └────────────┘ ┴
src ┴ ┴ └─────────────────────────┘ ┴ └────────────┘
typ ┴ ┴ ┴ ┴ └─────────────────────────┘ ┴ └────────────┘ ┴
591 have a = 0 ∨ b = 0, from mul_eq_zero_iff_eq_zero_or_eq_zero.1 this,
id ┴ ┴ ┴ ┴ ┴ └────────────────────────────────┘┴ └──┘
src ┴ ┴ ┴ └────────────────────────────────┘┴
typ ┴ ┴ ┴ ┴ ┴ └────────────────────────────────┘┴ └──┘
592 this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))
id └──┘└──┘ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└───┘ ┴ └─┘
src └──┘ └───┘ ┴ └─┘ └───┘ ┴ └─┘
typ └──┘└──┘ ┴ ┴└───┘ ┴ └─┘ ┴ ┴└───┘ ┴ └─┘
593 (by simp [or_imp_distrib] {contextual := tt})
id └────────────┘ └┘
src └────┘└────────────┘└┘ └────────────┘└┘┴
typ └────┘└────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └────────────┘ ┴
par └────┘ └┘ └────────────┘ ┴
pid ┴┴ ┴┴ └────────────┘ ┴
st └───────────────────────────────────────┘
594
595 theorem prod_eq_zero_iff {s : multiset (associates α)} :
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
doc └──────┘
596 s.prod = 0 ↔ (0 : associates α) ∈ s :=
id ┴└───┘ ┴ ┴ └────────┘ ┴ ┴ ┴
src └───┘ ┴ ┴ └────────┘ ┴
typ ┴└───┘ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └───┘
597 multiset.induction_on s (by simp; exact zero_ne_one.symm) $
id └───────────────────┘ ┴ └──────────────┘
src └───────────────────┘ └──┘ └────┘└──────────────┘
typ └───────────────────┘ ┴ └──┘ └────┘└──────────────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴
st └───────────────────────────┘
598 assume a s, by simp [mul_eq_zero_iff, @eq_comm _ 0 a] {contextual := tt}
id ┴ ┴ └─────────────┘ └─────┘ ┴ └┘
src └────┘└─────────────┘└┘ └─────┘└───┘ └┘ └────────────┘└┘└─
typ ┴ ┴ └────┘└─────────────┘└┘ └─────┘└───┘┴└┘ └────────────┘└┘└─
doc └────┘ └┘ └───┘ └┘ └────────────┘ └─
txt └────┘ └┘ └───┘ └┘ └────────────┘ └─
par └────┘ └┘ └───┘ └┘ └────────────┘ └─
pid ┴┴ └┘ └───┘ ┴┴ └────────────┘ ┴└
st └──────────────────────────────────────────────────────────
599
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
600 theorem irreducible_mk_iff (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
id ┴ └─────────┘ └───────────┘ ┴ ┴ └─────────┘ ┴
src └─────────┘ └───────────┘ ┴ └─────────┘
typ ┴ └─────────┘ └───────────┘ ┴ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
601 begin
st └─────
602 simp [irreducible, is_unit_mk],
id └─────────┘ └────────┘
src └────┘└─────────┘└┘└────────┘┴
typ └────┘└─────────┘└┘└────────┘┴
doc └────┘└─────────┘└┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ───────────────────────────────┘└─
603 apply and_congr iff.rfl,
id └───────┘ └─────┘
src └────┘└───────┘┴└─────┘
typ └────┘└───────┘┴└─────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────┘└─
604 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
605 { assume h x y eq,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ───┘└─────────────┘└─
606 have : is_unit (associates.mk x) ∨ is_unit (associates.mk y),
id ┴ └─────┘ └───────────┘ ┴
src └─────┘ ┴ ┴ └┘ ┴└─────┘┴ └───────────┘┴ ┴
typ └─────┘ ┴ ┴┴└┘ ┴└─────┘┴ └───────────┘┴┴┴
doc └─────┘ ┴ ┴ └┘ ┴└─────┘┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└─
607 from h _ _ (by rw [eq]; refl),
id ┴ └┘
src └───┘ └───┘ ┴└──┘└┘┴└┘└──┘┴
typ └───┘┴└───┘ ┴└──┘└┘┴└┘└──┘┴
doc └───┘ └───┘ ┴└──┘ ┴└┘└──┘┴
txt └───┘ └───┘ ┴└──┘ ┴└┘└──┘┴
par └───┘ └───┘ ┴└──┘ ┴└┘└──┘┴
pid └───┘ └───┘ └───┘ └──────┘
st ───────────────────┘└─────┘┴└────┘┴└─
608 simpa [is_unit_mk] },
id └────────┘
src └─────┘└────────┘└┘
typ └─────┘└────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴┴ ┴┴
st ──────────────────────┘└┘└
609 { refine assume h x y, quotient.induction_on₂ x y (assume x y eq, _),
id └────────────────────┘
src └─────┘ └──────┘└────────────────────┘┴ ┴ ┴ └─────────┘
typ └─────┘ └──────┘└────────────────────┘┴ ┴ ┴ └─────────┘
doc └─────┘ └──────┘ ┴ ┴ ┴ └─────────┘
txt └─────┘ └──────┘ ┴ ┴ ┴ └─────────┘
par └─────┘ └──────┘ ┴ ┴ ┴ └─────────┘
pid ┴ └──────┘ ┴ ┴ ┴ └─────────┘
st ─────────────────────────────────────────────────────────────────────┘└─
610 rcases quotient.exact eq.symm with ⟨u, eq⟩,
id └────────────┘ └─────┘
src └─────┘└────────────┘┴└─────┘└───────────┘
typ └─────┘└────────────┘┴└─────┘└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ─────────────────────────────────────────────┘└─
611 have : a = x * (y * u), by rwa [mul_assoc, eq_comm] at eq,
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────┘
src └─────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ └───┘└───────┘└┘└─────┘└─────┘
typ └─────┘┴┴┴┴┴┴┴┴ ┴┴ ┴┴┴ └───┘└───────┘└┘└─────┘└─────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘ └─────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘ └─────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └┘ └─────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴└────┘
st ─────────────────────────┘ └───────┘└───────┘┴ └─
612 show is_unit (associates.mk x) ∨ is_unit (associates.mk y),
id ┴ └─────┘ └───────────┘ ┴
src └───┘ ┴ ┴ └┘ ┴└─────┘┴ └───────────┘┴ ┴
typ └───┘ ┴ ┴┴└┘ ┴└─────┘┴ └───────────┘┴┴┴
doc └───┘ ┴ ┴ └┘ ┴└─────┘┴ ┴ ┴
txt └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
613 simpa [is_unit_mk] using h _ _ this }
id └────────┘ ┴ └──┘
src └─────┘└────────┘└──────┘ └───┘ ┴
typ └─────┘└────────┘└──────┘┴└───┘└──┘┴
doc └─────┘ └──────┘ └───┘ ┴
txt └─────┘ └──────┘ └───┘ ┴
par └─────┘ └──────┘ └───┘ ┴
pid ┴┴ ┴┴└────┘ └───┘ ┴
st ───────────────────────────────────────┘└─
614 end
st ──┘
615
616 lemma eq_of_mul_eq_mul_left :
617 ∀(a b c : associates α), a ≠ 0 → a * b = a * c → b = c :=
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
618 begin
st └─────
619 rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └───────────────┘
st ─────────────────────────┘└─
620 rcases quotient.exact' h with ⟨u, hu⟩,
id └─────────────┘ ┴
src └─────┘└─────────────┘┴ └───────────┘
typ └─────┘└─────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ──────────────────────────────────────┘└─
621 have hu : a * (b * ↑u) = a * c, { rwa [← mul_assoc] },
id ┴ ┴ ┴┴ ┴ ┴ ┴ └───────┘
src └────────┘ ┴┴┴ ┴ ┴┴ └┘┴┴ ┴ ┴ └─────┘└───────┘└┘
typ └────────┘ ┴┴┴ ┴┴ ┴┴┴└┘┴┴┴┴ ┴┴ └─────┘└───────┘└┘
doc └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ └┘
txt └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ └┘
par └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ └┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴┴
st ───────────────────────────────┘└──┘└──────────────┘┴┴└┘└
622 exact quotient.sound' ⟨u, eq_of_mul_eq_mul_left (mt (mk_zero_eq a).2 ha) hu⟩
id └─────────────┘ ┴ └───────────────────┘ └┘ └────────┘ ┴ └┘ └┘
src └────┘└─────────────┘┴ └┘└───────────────────┘┴ └┘┴ └────────┘┴ └──┘ └┘ └┘
typ └────┘└─────────────┘┴ ┴└┘└───────────────────┘┴ └┘┴ └────────┘┴┴└──┘└┘└┘└┘└┘
doc └────┘ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
txt └────┘ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
par └────┘ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
pid ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ ┴┴
st ──────────────────────────────────────────────────────────────────────────────┘
623 end
st └─┘
624
625 lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
626 a * b ≤ a * c → b ≤ c
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
627 | ⟨d, hd⟩ := ⟨d, eq_of_mul_eq_mul_left a _ _ ha $ by rwa ← mul_assoc⟩
id ┴ └───────────────────┘ ┴ └┘ └───────┘
src └───────────────────┘ └────┘└───────┘
typ ┴ └───────────────────┘ ┴ └┘ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid └─┘
st └──────────────┘
628
629 lemma one_or_eq_of_le_of_prime :
630 ∀(p m : associates α), prime p → m ≤ p → (m = 1 ∨ m = p)
id ┴ └────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴ ┴ ┴ ┴
typ ┴ └────────┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
631 | _ m ⟨hp0, hp1, h⟩ ⟨d, rfl⟩ :=
id ┴ ┴ ┴ └─┘
src └─┘
typ ┴ ┴ ┴ └─┘
632 match h m d (le_refl _) with
id └─────┘
src └─────┘
typ └─────┘
633 | or.inl h := classical.by_cases (assume : m = 0, by simp [this]) $
id └────┘ └────────────────┘ ┴ └──┘
src └────┘ └────────────────┘ ┴ └────┘ ┴
typ └────┘ └────────────────┘ ┴ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────┘
634 assume : m ≠ 0,
id ┴
src ┴
typ ┴
635 have m * d ≤ m * 1, by simpa using h,
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ └──────────┘┴
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────┘
636 have d ≤ 1, from associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this,
id ┴ └──────────────────────────────┘ ┴ ┴ ┴ └──┘
src ┴ └──────────────────────────────┘ ┴ ┴ ┴
typ ┴ └──────────────────────────────┘ ┴ ┴ ┴ └──┘
doc ┴ ┴
637 have d = 1, from lattice.bot_unique this,
id ┴ └────────────────┘ └──┘
src ┴ └────────────────┘
typ ┴ └────────────────┘ └──┘
638 by simp [this]
id └──┘
src └────┘ └┘
typ └────┘└──┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └───────────┘
639 | or.inr h := classical.by_cases (assume : d = 0, by simp [this] at hp0; contradiction) $
id └────┘ └────────────────┘ ┴ └──┘
src └────┘ └────────────────┘ ┴ └────┘ └──────┘ └───────────┘
typ └────┘ └────────────────┘ ┴ └────┘└──┘└──────┘ └───────────┘
doc └────┘ └──────┘ └───────────┘
txt └────┘ └──────┘ └───────────┘
par └────┘ └──────┘ └───────────┘
pid ┴┴ ┴┴└────┘
st └────────────────────────────────┘
640 assume : d ≠ 0,
id ┴
src ┴
typ ┴
641 have d * m ≤ d * 1, by simpa [mul_comm] using h,
id ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ └─────┘└──────┘└──────┘
typ ┴ ┴ ┴ └─────┘└──────┘└──────┘┴
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────┘
642 or.inl $ lattice.bot_unique $ associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
id └────┘ └────────────────┘ └──────────────────────────────┘ ┴ ┴ ┴ └──┘
src └────┘ └────────────────┘ └──────────────────────────────┘ ┴ ┴ ┴
typ └────┘ └────────────────┘ └──────────────────────────────┘ ┴ ┴ ┴ └──┘
doc ┴ ┴
643 end
644
645 end integral_domain
646
647 end associates